# Interaction of big operators with piecewise functions #

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

source
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 ⋯)
source
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 ⋯)
source
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)
source
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)
source
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 ⋯
source
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 ⋯
source
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
source
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
source
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 ⋯
source
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 ⋯
source
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
source
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
source
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 ⋯
source
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 ⋯
source
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
source
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
source
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)
source
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)
source
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)
source
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)
source
@[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
source
@[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
source
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
source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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.

source
@[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.

source
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
source
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
source
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.

source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
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
source
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
source
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
source
theorem Finset.sum_inter_add_sum_diff {ι : 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
source
theorem Finset.prod_eq_mul_prod_diff_singleton {ι : 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
source
theorem Finset.sum_eq_add_sum_diff_singleton {ι : 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
source
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
source
theorem Finset.sum_eq_sum_diff_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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
@[deprecated Finset.sum_update_of_notMem (since := "2025-05-23")]
theorem Finset.sum_update_of_not_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 = ∑ x ∈ s, f x

Alias of `Finset.sum_update_of_notMem`.

source
@[deprecated Finset.prod_update_of_notMem (since := "2025-05-23")]
theorem Finset.prod_update_of_not_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 = ∏ x ∈ s, f x

Alias of `Finset.prod_update_of_notMem`.

source
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
source
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
source
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`.

source
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`.

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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`.

source
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`.

source
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'`.

source
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'`.

source
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`.

source
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`.

source
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'`.

source
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'`.

source
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`.

source
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`.

source
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'`.

source
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'`.