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_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} [DecidablePred fun (x : α) => ¬p x] (f : (x : α) → p x → γ) (g : (x : α) → ¬p x → γ) (h : γ → β) : ∏ x ∈ s, h (if hx : p x then f x hx else g x hx) = (∏ x : { x : α // x ∈ {x ∈ s | p x} }, h (f ↑x ⋯)) * ∏ x : { x : α // x ∈ {x ∈ s | ¬p x} }, h (g ↑x ⋯)

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

theorem Finset.prod_apply_ite {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] {s : Finset α} {p : α → Prop} {_hp : DecidablePred p} (f g : α → γ) (h : γ → β) : ∏ 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_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] {s : Finset α} {p : α → Prop} {_hp : DecidablePred p} (f g : α → γ) (h : γ → β) : ∑ 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_3} {β : Type u_4} [CommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f : (x : α) → p x → β) (g : (x : α) → ¬p x → β) : (∏ x ∈ s, if hx : p x then f x hx else g x hx) = (∏ x : { x : α // x ∈ {x ∈ s | p x} }, f ↑x ⋯) * ∏ x : { x : α // x ∈ {x ∈ s | ¬p x} }, g ↑x ⋯

theorem Finset.sum_dite {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f : (x : α) → p x → β) (g : (x : α) → ¬p x → β) : (∑ x ∈ s, if hx : p x then f x hx else g x hx) = ∑ x : { x : α // x ∈ {x ∈ s | p x} }, f ↑x ⋯ + ∑ x : { x : α // x ∈ {x ∈ s | ¬p x} }, g ↑x ⋯

theorem Finset.prod_ite {α : Type u_3} {β : Type u_4} [CommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f g : α → β) : (∏ 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_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f g : α → β) : (∑ 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_3} {β : Type u_4} {s : Finset α} [CommMonoid β] {p : α → Prop} {x✝ : DecidablePred p} (h : ∀ i ∈ s, ¬p i) (f : (i : α) → p i → β) (g : (i : α) → ¬p i → β) : (∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i : { x : α // x ∈ s }, g ↑i ⋯

theorem Finset.sum_dite_of_false {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] {p : α → Prop} {x✝ : DecidablePred p} (h : ∀ i ∈ s, ¬p i) (f : (i : α) → p i → β) (g : (i : α) → ¬p i → β) : (∑ i ∈ s, if hi : p i then f i hi else g i hi) = ∑ i : { x : α // x ∈ s }, g ↑i ⋯

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

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

theorem Finset.prod_dite_of_true {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] {p : α → Prop} {x✝ : DecidablePred p} (h : ∀ i ∈ s, p i) (f : (i : α) → p i → β) (g : (i : α) → ¬p i → β) : (∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i : { x : α // x ∈ s }, f ↑i ⋯

theorem Finset.sum_dite_of_true {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] {p : α → Prop} {x✝ : DecidablePred p} (h : ∀ i ∈ s, p i) (f : (i : α) → p i → β) (g : (i : α) → ¬p i → β) : (∑ i ∈ s, if hi : p i then f i hi else g i hi) = ∑ i : { x : α // x ∈ s }, f ↑i ⋯

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

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

theorem Finset.prod_apply_ite_of_false {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Finset α} [CommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f g : α → γ) (k : γ → β) (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_3} {β : Type u_4} {γ : Type u_5} {s : Finset α} [AddCommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f g : α → γ) (k : γ → β) (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_3} {β : Type u_4} {γ : Type u_5} {s : Finset α} [CommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f g : α → γ) (k : γ → β) (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_3} {β : Type u_4} {γ : Type u_5} {s : Finset α} [AddCommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f g : α → γ) (k : γ → β) (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_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s t : Finset α) (f : α → β) : (∏ i ∈ s, if i ∈ t then f i else 1) = ∏ i ∈ s ∩ t, f i

@[simp]

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

theorem Finset.prod_attach_eq_prod_dite {α : Type u_3} {β : Type u_4} [CommMonoid β] [Fintype α] (s : Finset α) (f : { x : α // x ∈ s } → β) [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_3} {β : Type u_4} [AddCommMonoid β] [Fintype α] (s : Finset α) (f : { x : α // x ∈ s } → β) [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_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : (x : α) → a = x → β) : (∏ 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_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : (x : α) → a = x → β) : (∑ 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_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : (x : α) → x = a → β) : (∏ 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_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : (x : α) → x = a → β) : (∑ 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_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : α → β) : (∏ 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_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : α → β) : (∑ 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_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : α → β) : (∏ 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_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : α → β) : (∑ 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_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : α → β) (h : a ∈ s) : (∏ x ∈ s, if a = x then b x else 1) = b a

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

theorem Finset.prod_ite_eq_of_mem' {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : α → β) (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_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : α → β) (h : a ∈ s) : (∑ x ∈ s, if x = a then b x else 0) = b a

@[simp]

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

@[simp]

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

@[simp]

theorem Finset.prod_pi_mulSingle {α : Type u_3} {β : α → Type u_6} [DecidableEq α] [(a : α) → CommMonoid (β a)] (a : α) (f : (a : α) → β 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_3} {β : α → Type u_6} [DecidableEq α] [(a : α) → AddCommMonoid (β a)] (a : α) (f : (a : α) → β 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_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s t : Finset α) (f g : α → β) : ∏ x ∈ s, t.piecewise f g x = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g x

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

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

theorem Finset.sum_inter_add_sum_diff {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s t : Finset α) (f : α → β) : ∑ x ∈ s ∩ t, f x + ∑ x ∈ s \ t, f x = ∑ x ∈ s, f x

theorem Finset.prod_eq_mul_prod_diff_singleton {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) : ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

theorem Finset.sum_eq_add_sum_diff_singleton {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) : ∑ x ∈ s, f x = f i + ∑ x ∈ s \ {i}, f x

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

theorem Finset.sum_eq_sum_diff_singleton_add {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) : ∑ x ∈ s, f x = ∑ x ∈ s \ {i}, f x + f i

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

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

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

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

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

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

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

@[deprecated Finset.sum_update_of_notMem (since := "2025-05-23")]

theorem Finset.sum_update_of_not_mem {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] {s : Finset α} {i : α} (h : i ∉ s) (f : α → β) (b : β) : ∑ x ∈ s, Function.update f i b x = ∑ x ∈ s, f x

Alias of Finset.sum_update_of_notMem.

@[deprecated Finset.prod_update_of_notMem (since := "2025-05-23")]

theorem Finset.prod_update_of_not_mem {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] {s : Finset α} {i : α} (h : i ∉ s) (f : α → β) (b : β) : ∏ x ∈ s, Function.update f i b x = ∏ x ∈ s, f x

Alias of Finset.prod_update_of_notMem.

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

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

theorem Finset.prod_ite_one {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (p : α → Prop) [DecidablePred p] (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) (a : β) : (∏ 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_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (p : α → Prop) [DecidablePred p] (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) (a : β) : (∑ 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_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (f : α → β) (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_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (f : α → β) (a : α) : ∑ x ∈ s, (if a = x then 1 else 0) • f x = if a ∈ s then f a else 0

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} {α : Type u_3} [CommMonoid α] [Fintype ι] (p : ι → Prop) [DecidablePred p] (h : ∀ (i j : ι), p i → p j → i = j) (a : α) : (∏ 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} {α : Type u_3} [AddCommMonoid α] [Fintype ι] (p : ι → Prop) [DecidablePred p] (h : ∀ (i j : ι), p i → p j → i = j) (a : α) : (∑ i : ι, if p i then a else 0) = if ∃ (i : ι), p i then a else 0

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

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

theorem Fintype.prod_dite_eq {ι : Type u_1} {α : Type u_3} [CommMonoid α] [Fintype ι] [DecidableEq ι] (i : ι) (f : (j : ι) → i = j → α) : (∏ 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} {α : Type u_3} [AddCommMonoid α] [Fintype ι] [DecidableEq ι] (i : ι) (f : (j : ι) → i = j → α) : (∑ 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} {α : Type u_3} [CommMonoid α] [Fintype ι] [DecidableEq ι] (i : ι) (f : (j : ι) → j = i → α) : (∏ 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} {α : Type u_3} [AddCommMonoid α] [Fintype ι] [DecidableEq ι] (i : ι) (f : (j : ι) → j = i → α) : (∑ 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} {α : Type u_3} [CommMonoid α] [Fintype ι] [DecidableEq ι] (i : ι) (f : ι → α) : (∏ 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} {α : Type u_3} [AddCommMonoid α] [Fintype ι] [DecidableEq ι] (i : ι) (f : ι → α) : (∑ 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} {α : Type u_3} [CommMonoid α] [Fintype ι] [DecidableEq ι] (i : ι) (f : ι → α) : (∏ 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} {α : Type u_3} [AddCommMonoid α] [Fintype ι] [DecidableEq ι] (i : ι) (f : ι → α) : (∑ 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 ι] {α : ι → Type u_6} [(i : ι) → CommMonoid (α i)] (i : ι) (f : (i : ι) → α 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 ι] {α : ι → Type u_6} [(i : ι) → AddCommMonoid (α i)] (i : ι) (f : (i : ι) → α i) : ∑ j : ι, Pi.single j (f j) i = f i

See also Finset.sum_pi_single.

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

See also Finset.prod_pi_mulSingle'.

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

See also Finset.sum_pi_single'.