Interaction of big operators with piecewise functions

This file proves lemmas on the sum and product of piecewise functions, including ite and dite.

theorem Finset.prod_apply_dite {ι : Type u_1} {M : Type u_3} {γ : Type u_5} {s : Finset ι} [CommMonoid M] {p : ι → Prop} [DecidablePred p] [DecidablePred fun (x : ι) => ¬p x] (f : (x : ι) → p x → γ) (g : (x : ι) → ¬p x → γ) (h : γ → M) : ∏ x ∈ s, h (if hx : p x then f x hx else g x hx) = (∏ x : ↥({x ∈ s | p x}), h (f ↑x ⋯)) * ∏ x : ↥({x ∈ s | ¬p x}), h (g ↑x ⋯)

theorem Finset.sum_apply_dite {ι : Type u_1} {M : Type u_3} {γ : Type u_5} {s : Finset ι} [AddCommMonoid M] {p : ι → Prop} [DecidablePred p] [DecidablePred fun (x : ι) => ¬p x] (f : (x : ι) → p x → γ) (g : (x : ι) → ¬p x → γ) (h : γ → M) : ∑ x ∈ s, h (if hx : p x then f x hx else g x hx) = ∑ x : ↥({x ∈ s | p x}), h (f ↑x ⋯) + ∑ x : ↥({x ∈ s | ¬p x}), h (g ↑x ⋯)

theorem Finset.prod_apply_ite {ι : Type u_1} {M : Type u_3} {γ : Type u_5} [CommMonoid M] {s : Finset ι} {p : ι → Prop} [DecidablePred p] (f g : ι → γ) (h : γ → M) : ∏ x ∈ s, h (if p x then f x else g x) = (∏ x ∈ s with p x, h (f x)) * ∏ x ∈ s with ¬p x, h (g x)

theorem Finset.sum_apply_ite {ι : Type u_1} {M : Type u_3} {γ : Type u_5} [AddCommMonoid M] {s : Finset ι} {p : ι → Prop} [DecidablePred p] (f g : ι → γ) (h : γ → M) : ∑ x ∈ s, h (if p x then f x else g x) = ∑ x ∈ s with p x, h (f x) + ∑ x ∈ s with ¬p x, h (g x)

theorem Finset.prod_dite {ι : Type u_1} {M : Type u_3} [CommMonoid M] {s : Finset ι} {p : ι → Prop} [DecidablePred p] (f : (x : ι) → p x → M) (g : (x : ι) → ¬p x → M) : (∏ x ∈ s, if hx : p x then f x hx else g x hx) = (∏ x : ↥({x ∈ s | p x}), f ↑x ⋯) * ∏ x : ↥({x ∈ s | ¬p x}), g ↑x ⋯

theorem Finset.sum_dite {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] {s : Finset ι} {p : ι → Prop} [DecidablePred p] (f : (x : ι) → p x → M) (g : (x : ι) → ¬p x → M) : (∑ x ∈ s, if hx : p x then f x hx else g x hx) = ∑ x : ↥({x ∈ s | p x}), f ↑x ⋯ + ∑ x : ↥({x ∈ s | ¬p x}), g ↑x ⋯

theorem Finset.prod_ite {ι : Type u_1} {M : Type u_3} [CommMonoid M] {s : Finset ι} {p : ι → Prop} [DecidablePred p] (f g : ι → M) : (∏ x ∈ s, if p x then f x else g x) = (∏ x ∈ s with p x, f x) * ∏ x ∈ s with ¬p x, g x

theorem Finset.sum_ite {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] {s : Finset ι} {p : ι → Prop} [DecidablePred p] (f g : ι → M) : (∑ x ∈ s, if p x then f x else g x) = ∑ x ∈ s with p x, f x + ∑ x ∈ s with ¬p x, g x

theorem Finset.prod_dite_of_false {ι : Type u_1} {M : Type u_3} {s : Finset ι} [CommMonoid M] {p : ι → Prop} [DecidablePred p] (h : ∀ i ∈ s, ¬p i) (f : (i : ι) → p i → M) (g : (i : ι) → ¬p i → M) : (∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i : ↥s, g ↑i ⋯

theorem Finset.sum_dite_of_false {ι : Type u_1} {M : Type u_3} {s : Finset ι} [AddCommMonoid M] {p : ι → Prop} [DecidablePred p] (h : ∀ i ∈ s, ¬p i) (f : (i : ι) → p i → M) (g : (i : ι) → ¬p i → M) : (∑ i ∈ s, if hi : p i then f i hi else g i hi) = ∑ i : ↥s, g ↑i ⋯

theorem Finset.prod_ite_of_false {ι : Type u_1} {M : Type u_3} {s : Finset ι} [CommMonoid M] {p : ι → Prop} [DecidablePred p] (h : ∀ x ∈ s, ¬p x) (f g : ι → M) : (∏ x ∈ s, if p x then f x else g x) = ∏ x ∈ s, g x

theorem Finset.sum_ite_of_false {ι : Type u_1} {M : Type u_3} {s : Finset ι} [AddCommMonoid M] {p : ι → Prop} [DecidablePred p] (h : ∀ x ∈ s, ¬p x) (f g : ι → M) : (∑ x ∈ s, if p x then f x else g x) = ∑ x ∈ s, g x

theorem Finset.prod_dite_of_true {ι : Type u_1} {M : Type u_3} {s : Finset ι} [CommMonoid M] {p : ι → Prop} [DecidablePred p] (h : ∀ i ∈ s, p i) (f : (i : ι) → p i → M) (g : (i : ι) → ¬p i → M) : (∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i : ↥s, f ↑i ⋯

theorem Finset.sum_dite_of_true {ι : Type u_1} {M : Type u_3} {s : Finset ι} [AddCommMonoid M] {p : ι → Prop} [DecidablePred p] (h : ∀ i ∈ s, p i) (f : (i : ι) → p i → M) (g : (i : ι) → ¬p i → M) : (∑ i ∈ s, if hi : p i then f i hi else g i hi) = ∑ i : ↥s, f ↑i ⋯

theorem Finset.prod_ite_of_true {ι : Type u_1} {M : Type u_3} {s : Finset ι} [CommMonoid M] {p : ι → Prop} [DecidablePred p] (h : ∀ x ∈ s, p x) (f g : ι → M) : (∏ x ∈ s, if p x then f x else g x) = ∏ x ∈ s, f x

theorem Finset.sum_ite_of_true {ι : Type u_1} {M : Type u_3} {s : Finset ι} [AddCommMonoid M] {p : ι → Prop} [DecidablePred p] (h : ∀ x ∈ s, p x) (f g : ι → M) : (∑ x ∈ s, if p x then f x else g x) = ∑ x ∈ s, f x

theorem Finset.prod_apply_ite_of_false {ι : Type u_1} {M : Type u_3} {γ : Type u_5} {s : Finset ι} [CommMonoid M] {p : ι → Prop} [DecidablePred p] (f g : ι → γ) (k : γ → M) (h : ∀ x ∈ s, ¬p x) : ∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (g x)

theorem Finset.sum_apply_ite_of_false {ι : Type u_1} {M : Type u_3} {γ : Type u_5} {s : Finset ι} [AddCommMonoid M] {p : ι → Prop} [DecidablePred p] (f g : ι → γ) (k : γ → M) (h : ∀ x ∈ s, ¬p x) : ∑ x ∈ s, k (if p x then f x else g x) = ∑ x ∈ s, k (g x)

theorem Finset.prod_apply_ite_of_true {ι : Type u_1} {M : Type u_3} {γ : Type u_5} {s : Finset ι} [CommMonoid M] {p : ι → Prop} [DecidablePred p] (f g : ι → γ) (k : γ → M) (h : ∀ x ∈ s, p x) : ∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (f x)

theorem Finset.sum_apply_ite_of_true {ι : Type u_1} {M : Type u_3} {γ : Type u_5} {s : Finset ι} [AddCommMonoid M] {p : ι → Prop} [DecidablePred p] (f g : ι → γ) (k : γ → M) (h : ∀ x ∈ s, p x) : ∑ x ∈ s, k (if p x then f x else g x) = ∑ x ∈ s, k (f x)

@[simp]

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

@[simp]

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

theorem Finset.prod_attach_eq_prod_dite {ι : Type u_1} {M : Type u_3} [CommMonoid M] [Fintype ι] (s : Finset ι) (f : ↥s → M) [DecidablePred fun (x : ι) => x ∈ s] : ∏ i ∈ s.attach, f i = ∏ i : ι, if h : i ∈ s then f ⟨i, h⟩ else 1

theorem Finset.sum_attach_eq_sum_dite {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Fintype ι] (s : Finset ι) (f : ↥s → M) [DecidablePred fun (x : ι) => x ∈ s] : ∑ i ∈ s.attach, f i = ∑ i : ι, if h : i ∈ s then f ⟨i, h⟩ else 0

@[simp]

theorem Finset.prod_dite_eq {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] (s : Finset ι) (a : ι) (b : (x : ι) → a = x → M) : (∏ x ∈ s, if h : a = x then b x h else 1) = if a ∈ s then b a ⋯ else 1

@[simp]

theorem Finset.sum_dite_eq {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [DecidableEq ι] (s : Finset ι) (a : ι) (b : (x : ι) → a = x → M) : (∑ x ∈ s, if h : a = x then b x h else 0) = if a ∈ s then b a ⋯ else 0

@[simp]

theorem Finset.prod_dite_eq' {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] (s : Finset ι) (a : ι) (b : (x : ι) → x = a → M) : (∏ x ∈ s, if h : x = a then b x h else 1) = if a ∈ s then b a ⋯ else 1

@[simp]

theorem Finset.sum_dite_eq' {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [DecidableEq ι] (s : Finset ι) (a : ι) (b : (x : ι) → x = a → M) : (∑ x ∈ s, if h : x = a then b x h else 0) = if a ∈ s then b a ⋯ else 0

@[simp]

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

@[simp]

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

@[simp]

theorem Finset.prod_ite_eq' {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] (s : Finset ι) (a : ι) (b : ι → M) : (∏ x ∈ s, if x = a then b x else 1) = if a ∈ s then b a else 1

A product taken over a conditional whose condition is an equality test on the index and whose alternative is 1 has value either the term at that index or 1.

The difference with Finset.prod_ite_eq is that the arguments to Eq are swapped.

@[simp]

theorem Finset.sum_ite_eq' {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [DecidableEq ι] (s : Finset ι) (a : ι) (b : ι → M) : (∑ x ∈ s, if x = a then b x else 0) = if a ∈ s then b a else 0

A sum taken over a conditional whose condition is an equality test on the index and whose alternative is 0 has value either the term at that index or 0.

The difference with Finset.sum_ite_eq is that the arguments to Eq are swapped.

theorem Finset.prod_ite_eq_of_mem {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] (s : Finset ι) (a : ι) (b : ι → M) (h : a ∈ s) : (∏ x ∈ s, if a = x then b x else 1) = b a

theorem Finset.sum_ite_eq_of_mem {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [DecidableEq ι] (s : Finset ι) (a : ι) (b : ι → M) (h : a ∈ s) : (∑ x ∈ s, if a = x then b x else 0) = b a

theorem Finset.prod_ite_eq_of_mem' {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] (s : Finset ι) (a : ι) (b : ι → M) (h : a ∈ s) : (∏ x ∈ s, if x = a then b x else 1) = b a

The difference with Finset.prod_ite_eq_of_mem is that the arguments to Eq are swapped.

theorem Finset.sum_ite_eq_of_mem' {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [DecidableEq ι] (s : Finset ι) (a : ι) (b : ι → M) (h : a ∈ s) : (∑ x ∈ s, if x = a then b x else 0) = b a

@[simp]

theorem Finset.prod_pi_mulSingle' {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] (a : ι) (x : M) (s : Finset ι) : ∏ a' ∈ s, Pi.mulSingle a x a' = if a ∈ s then x else 1

@[simp]

theorem Finset.sum_pi_single' {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [DecidableEq ι] (a : ι) (x : M) (s : Finset ι) : ∑ a' ∈ s, Pi.single a x a' = if a ∈ s then x else 0

@[simp]

theorem Finset.prod_pi_mulSingle {ι : Type u_1} {M : ι → Type u_6} [DecidableEq ι] [(a : ι) → CommMonoid (M a)] (a : ι) (f : (a : ι) → M a) (s : Finset ι) : ∏ a' ∈ s, Pi.mulSingle a' (f a') a = if a ∈ s then f a else 1

@[simp]

theorem Finset.sum_pi_single {ι : Type u_1} {M : ι → Type u_6} [DecidableEq ι] [(a : ι) → AddCommMonoid (M a)] (a : ι) (f : (a : ι) → M a) (s : Finset ι) : ∑ a' ∈ s, Pi.single a' (f a') a = if a ∈ s then f a else 0

theorem Finset.prod_piecewise {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] (s t : Finset ι) (f g : ι → M) : ∏ x ∈ s, t.piecewise f g x = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g x

theorem Finset.sum_piecewise {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [DecidableEq ι] (s t : Finset ι) (f g : ι → M) : ∑ x ∈ s, t.piecewise f g x = ∑ x ∈ s ∩ t, f x + ∑ x ∈ s \ t, g x

theorem Finset.prod_inter_mul_prod_sdiff {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] (s t : Finset ι) (f : ι → M) : (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, f x = ∏ x ∈ s, f x

theorem Finset.sum_inter_add_sum_sdiff {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [DecidableEq ι] (s t : Finset ι) (f : ι → M) : ∑ x ∈ s ∩ t, f x + ∑ x ∈ s \ t, f x = ∑ x ∈ s, f x

@[deprecated Finset.prod_inter_mul_prod_sdiff (since := "2026-06-03")]

theorem Finset.prod_inter_mul_prod_diff {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] (s t : Finset ι) (f : ι → M) : (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, f x = ∏ x ∈ s, f x

Alias of Finset.prod_inter_mul_prod_sdiff.

theorem Finset.prod_eq_mul_prod_sdiff_singleton {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] {s : Finset ι} (i : ι) (f : ι → M) (h : i ∉ s → f i = 1) : ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

theorem Finset.sum_eq_add_sum_sdiff_singleton {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [DecidableEq ι] {s : Finset ι} (i : ι) (f : ι → M) (h : i ∉ s → f i = 0) : ∑ x ∈ s, f x = f i + ∑ x ∈ s \ {i}, f x

@[deprecated Finset.prod_eq_mul_prod_sdiff_singleton (since := "2026-06-03")]

theorem Finset.prod_eq_mul_prod_diff_singleton {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] {s : Finset ι} (i : ι) (f : ι → M) (h : i ∉ s → f i = 1) : ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

Alias of Finset.prod_eq_mul_prod_sdiff_singleton.

theorem Finset.prod_eq_mul_prod_sdiff_singleton_of_mem {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] {s : Finset ι} {i : ι} (h : i ∈ s) (f : ι → M) : ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

theorem Finset.sum_eq_add_sum_sdiff_singleton_of_mem {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [DecidableEq ι] {s : Finset ι} {i : ι} (h : i ∈ s) (f : ι → M) : ∑ x ∈ s, f x = f i + ∑ x ∈ s \ {i}, f x

@[deprecated Finset.prod_eq_mul_prod_sdiff_singleton_of_mem (since := "2026-06-03")]

theorem Finset.prod_eq_mul_prod_diff_singleton_of_mem {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] {s : Finset ι} {i : ι} (h : i ∈ s) (f : ι → M) : ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

Alias of Finset.prod_eq_mul_prod_sdiff_singleton_of_mem.

theorem Finset.prod_eq_prod_sdiff_singleton_mul {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] {s : Finset ι} {i : ι} (h : i ∈ s) (f : ι → M) : ∏ x ∈ s, f x = (∏ x ∈ s \ {i}, f x) * f i

theorem Finset.sum_eq_sum_sdiff_singleton_add {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [DecidableEq ι] {s : Finset ι} {i : ι} (h : i ∈ s) (f : ι → M) : ∑ x ∈ s, f x = ∑ x ∈ s \ {i}, f x + f i

@[deprecated Finset.prod_eq_prod_sdiff_singleton_mul (since := "2026-06-03")]

theorem Finset.prod_eq_prod_diff_singleton_mul {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] {s : Finset ι} {i : ι} (h : i ∈ s) (f : ι → M) : ∏ x ∈ s, f x = (∏ x ∈ s \ {i}, f x) * f i

Alias of Finset.prod_eq_prod_sdiff_singleton_mul.

theorem Fintype.prod_eq_mul_prod_compl {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] [Fintype ι] (a : ι) (f : ι → M) : ∏ i : ι, f i = f a * ∏ i ∈ {a}ᶜ, f i

theorem Fintype.sum_eq_add_sum_compl {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [DecidableEq ι] [Fintype ι] (a : ι) (f : ι → M) : ∑ i : ι, f i = f a + ∑ i ∈ {a}ᶜ, f i

theorem Fintype.prod_eq_prod_compl_mul {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] [Fintype ι] (a : ι) (f : ι → M) : ∏ i : ι, f i = (∏ i ∈ {a}ᶜ, f i) * f a

theorem Fintype.sum_eq_sum_compl_add {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [DecidableEq ι] [Fintype ι] (a : ι) (f : ι → M) : ∑ i : ι, f i = ∑ i ∈ {a}ᶜ, f i + f a

theorem Finset.dvd_prod_of_mem {ι : Type u_1} {M : Type u_3} [CommMonoid M] (f : ι → M) {a : ι} {s : Finset ι} (ha : a ∈ s) : f a ∣ ∏ i ∈ s, f i

theorem Finset.prod_update_of_notMem {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] {s : Finset ι} {i : ι} (h : i ∉ s) (f : ι → M) (b : M) : ∏ x ∈ s, Function.update f i b x = ∏ x ∈ s, f x

theorem Finset.sum_update_of_notMem {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [DecidableEq ι] {s : Finset ι} {i : ι} (h : i ∉ s) (f : ι → M) (b : M) : ∑ x ∈ s, Function.update f i b x = ∑ x ∈ s, f x

theorem Finset.prod_update_of_mem {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] {s : Finset ι} {i : ι} (h : i ∈ s) (f : ι → M) (b : M) : ∏ x ∈ s, Function.update f i b x = b * ∏ x ∈ s \ {i}, f x

theorem Finset.sum_update_of_mem {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [DecidableEq ι] {s : Finset ι} {i : ι} (h : i ∈ s) (f : ι → M) (b : M) : ∑ x ∈ s, Function.update f i b x = b + ∑ x ∈ s \ {i}, f x

theorem Finset.prod_ite_one {ι : Type u_1} {M : Type u_3} [CommMonoid M] (s : Finset ι) (p : ι → Prop) [DecidablePred p] (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) (a : M) : (∏ i ∈ s, if p i then a else 1) = if ∃ i ∈ s, p i then a else 1

See also Finset.prod_ite_zero.

theorem Finset.sum_ite_zero {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (p : ι → Prop) [DecidablePred p] (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) (a : M) : (∑ i ∈ s, if p i then a else 0) = if ∃ i ∈ s, p i then a else 0

See also Finset.sum_boole.

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

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

theorem Finset.prod_eq_prod_iff_single {ι : Type u_1} {M : Type u_3} {s : Finset ι} [CommMonoid M] [IsRightCancelMul M] {f g : ι → M} {i : ι} (hi : i ∈ s) (hfg : ∀ j ∈ s, j ≠ i → f j = g j) : ∏ j ∈ s, f j = ∏ j ∈ s, g j ↔ f i = g i

theorem Finset.sum_eq_sum_iff_single {ι : Type u_1} {M : Type u_3} {s : Finset ι} [AddCommMonoid M] [IsRightCancelAdd M] {f g : ι → M} {i : ι} (hi : i ∈ s) (hfg : ∀ j ∈ s, j ≠ i → f j = g j) : ∑ j ∈ s, f j = ∑ j ∈ s, g j ↔ f i = g i

theorem Finset.card_filter {ι : Type u_1} (p : ι → Prop) [DecidablePred p] (s : Finset ι) : {i ∈ s | p i}.card = ∑ i ∈ s, if p i then 1 else 0

theorem Fintype.prod_ite_eq_ite_exists {ι : Type u_1} {M : Type u_3} [CommMonoid M] [Fintype ι] (p : ι → Prop) [DecidablePred p] (h : ∀ (i j : ι), p i → p j → i = j) (a : M) : (∏ i : ι, if p i then a else 1) = if ∃ (i : ι), p i then a else 1

theorem Fintype.sum_ite_eq_ite_exists {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Fintype ι] (p : ι → Prop) [DecidablePred p] (h : ∀ (i j : ι), p i → p j → i = j) (a : M) : (∑ i : ι, if p i then a else 0) = if ∃ (i : ι), p i then a else 0

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

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

theorem Fintype.prod_dite_eq {ι : Type u_1} {M : Type u_3} [CommMonoid M] [Fintype ι] [DecidableEq ι] (i : ι) (f : (j : ι) → i = j → M) : (∏ j : ι, if h : i = j then f j h else 1) = f i ⋯

See also Finset.prod_dite_eq.

theorem Fintype.sum_dite_eq {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Fintype ι] [DecidableEq ι] (i : ι) (f : (j : ι) → i = j → M) : (∑ j : ι, if h : i = j then f j h else 0) = f i ⋯

See also Finset.sum_dite_eq.

theorem Fintype.prod_dite_eq' {ι : Type u_1} {M : Type u_3} [CommMonoid M] [Fintype ι] [DecidableEq ι] (i : ι) (f : (j : ι) → j = i → M) : (∏ j : ι, if h : j = i then f j h else 1) = f i ⋯

See also Finset.prod_dite_eq'.

theorem Fintype.sum_dite_eq' {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Fintype ι] [DecidableEq ι] (i : ι) (f : (j : ι) → j = i → M) : (∑ j : ι, if h : j = i then f j h else 0) = f i ⋯

See also Finset.sum_dite_eq'.

theorem Fintype.prod_ite_eq {ι : Type u_1} {M : Type u_3} [CommMonoid M] [Fintype ι] [DecidableEq ι] (i : ι) (f : ι → M) : (∏ j : ι, if i = j then f j else 1) = f i

See also Finset.prod_ite_eq.

theorem Fintype.sum_ite_eq {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Fintype ι] [DecidableEq ι] (i : ι) (f : ι → M) : (∑ j : ι, if i = j then f j else 0) = f i

See also Finset.sum_ite_eq.

theorem Fintype.prod_ite_eq' {ι : Type u_1} {M : Type u_3} [CommMonoid M] [Fintype ι] [DecidableEq ι] (i : ι) (f : ι → M) : (∏ j : ι, if j = i then f j else 1) = f i

See also Finset.prod_ite_eq'.

theorem Fintype.sum_ite_eq' {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Fintype ι] [DecidableEq ι] (i : ι) (f : ι → M) : (∑ j : ι, if j = i then f j else 0) = f i

See also Finset.sum_ite_eq'.

theorem Fintype.prod_pi_mulSingle {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : ι → Type u_6} [(i : ι) → CommMonoid (M i)] (i : ι) (f : (i : ι) → M i) : ∏ j : ι, Pi.mulSingle j (f j) i = f i

See also Finset.prod_pi_mulSingle.

theorem Fintype.sum_pi_single {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : ι → Type u_6} [(i : ι) → AddCommMonoid (M i)] (i : ι) (f : (i : ι) → M i) : ∑ j : ι, Pi.single j (f j) i = f i

See also Finset.sum_pi_single.

theorem Fintype.prod_pi_mulSingle' {ι : Type u_1} {M : Type u_3} [CommMonoid M] [Fintype ι] [DecidableEq ι] (i : ι) (a : M) : ∏ j : ι, Pi.mulSingle i a j = a

See also Finset.prod_pi_mulSingle'.

theorem Fintype.sum_pi_single' {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Fintype ι] [DecidableEq ι] (i : ι) (a : M) : ∑ j : ι, Pi.single i a j = a

See also Finset.sum_pi_single'.