@[simp]

theorem Finset.prod_ite_not_mem {ι : Type u_1} {M : Type u_3} [CommMonoid M] (s t : Finset ι) [DecidableEq ι] (f : ι → M) : (∏ x ∈ s, if x ∈ t then 1 else f x) = ∏ x ∈ s \ t, f x

@[simp]

theorem Finset.sum_ite_not_mem {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s t : Finset ι) [DecidableEq ι] (f : ι → M) : (∑ x ∈ s, if x ∈ t then 0 else f x) = ∑ x ∈ s \ t, f x