# Documentation

Mathlib.Data.Fintype.BigOperators

Results about "big operations" over a Fintype, and consequent results about cardinalities of certain types.

## Implementation note #

This content had previously been in Data.Fintype.Basic, but was moved here to avoid requiring Algebra.BigOperators (and hence many other imports) as a dependency of Fintype.

However many of the results here really belong in Algebra.BigOperators.Basic and should be moved at some point.

theorem Fintype.sum_bool {α : Type u_1} [inst : ] (f : Boolα) :
(Finset.sum Finset.univ fun b => f b) = f true +
theorem Fintype.prod_bool {α : Type u_1} [inst : ] (f : Boolα) :
(Finset.prod Finset.univ fun b => f b) = f true *
theorem Fintype.card_eq_sum_ones {α : Type u_1} [inst : ] :
= Finset.sum Finset.univ fun _a => 1
theorem Fintype.sum_extend_by_zero {α : Type u_1} {ι : Type u_2} [inst : ] [inst : ] [inst : ] (s : ) (f : ια) :
(Finset.sum Finset.univ fun i => if i s then f i else 0) = Finset.sum s fun i => f i
theorem Fintype.prod_extend_by_one {α : Type u_1} {ι : Type u_2} [inst : ] [inst : ] [inst : ] (s : ) (f : ια) :
(Finset.prod Finset.univ fun i => if i s then f i else 1) = Finset.prod s fun i => f i
theorem Fintype.sum_eq_zero {α : Type u_2} {M : Type u_1} [inst : ] [inst : ] (f : αM) (h : ∀ (a : α), f a = 0) :
(Finset.sum Finset.univ fun a => f a) = 0
theorem Fintype.prod_eq_one {α : Type u_2} {M : Type u_1} [inst : ] [inst : ] (f : αM) (h : ∀ (a : α), f a = 1) :
(Finset.prod Finset.univ fun a => f a) = 1
theorem Fintype.sum_congr {α : Type u_2} {M : Type u_1} [inst : ] [inst : ] (f : αM) (g : αM) (h : ∀ (a : α), f a = g a) :
(Finset.sum Finset.univ fun a => f a) = Finset.sum Finset.univ fun a => g a
theorem Fintype.prod_congr {α : Type u_2} {M : Type u_1} [inst : ] [inst : ] (f : αM) (g : αM) (h : ∀ (a : α), f a = g a) :
(Finset.prod Finset.univ fun a => f a) = Finset.prod Finset.univ fun a => g a
theorem Fintype.sum_eq_single {α : Type u_1} {M : Type u_2} [inst : ] [inst : ] {f : αM} (a : α) (h : ∀ (x : α), x af x = 0) :
(Finset.sum Finset.univ fun x => f x) = f a
theorem Fintype.prod_eq_single {α : Type u_1} {M : Type u_2} [inst : ] [inst : ] {f : αM} (a : α) (h : ∀ (x : α), x af x = 1) :
(Finset.prod Finset.univ fun x => f x) = f a
theorem Fintype.sum_eq_add {α : Type u_1} {M : Type u_2} [inst : ] [inst : ] {f : αM} (a : α) (b : α) (h₁ : a b) (h₂ : ∀ (x : α), x a x bf x = 0) :
(Finset.sum Finset.univ fun x => f x) = f a + f b
theorem Fintype.prod_eq_mul {α : Type u_1} {M : Type u_2} [inst : ] [inst : ] {f : αM} (a : α) (b : α) (h₁ : a b) (h₂ : ∀ (x : α), x a x bf x = 1) :
(Finset.prod Finset.univ fun x => f x) = f a * f b
theorem Fintype.eq_of_subsingleton_of_sum_eq {M : Type u_2} [inst : ] {ι : Type u_1} [inst : ] {s : } {f : ιM} {b : M} (h : (Finset.sum s fun i => f i) = b) (i : ι) :
i sf i = b

If a sum of a Finset of a subsingleton type has a given value, so do the terms in that sum.

theorem Fintype.eq_of_subsingleton_of_prod_eq {M : Type u_2} [inst : ] {ι : Type u_1} [inst : ] {s : } {f : ιM} {b : M} (h : (Finset.prod s fun i => f i) = b) (i : ι) :
i sf i = b

If a product of a Finset of a subsingleton type has a given value, so do the terms in that product.

@[simp]
theorem Fintype.sum_option {α : Type u_1} {M : Type u_2} [inst : ] [inst : ] (f : M) :
(Finset.sum Finset.univ fun i => f i) = f none + Finset.sum Finset.univ fun i => f (some i)
@[simp]
theorem Fintype.prod_option {α : Type u_1} {M : Type u_2} [inst : ] [inst : ] (f : M) :
(Finset.prod Finset.univ fun i => f i) = f none * Finset.prod Finset.univ fun i => f (some i)
@[simp]
theorem Fintype.card_sigma {α : Type u_1} (β : αType u_2) [inst : ] [inst : (a : α) → Fintype (β a)] :
= Finset.sum Finset.univ fun a => Fintype.card (β a)
@[simp]
theorem Finset.card_pi {α : Type u_1} [inst : ] {δ : αType u_2} (s : ) (t : (a : α) → Finset (δ a)) :
Finset.card () = Finset.prod s fun a => Finset.card (t a)
@[simp]
theorem Fintype.card_piFinset {α : Type u_1} [inst : ] [inst : ] {δ : αType u_2} (t : (a : α) → Finset (δ a)) :
= Finset.prod Finset.univ fun a => Finset.card (t a)
@[simp]
theorem Fintype.card_pi {α : Type u_2} {β : αType u_1} [inst : ] [inst : ] [inst : (a : α) → Fintype (β a)] :
Fintype.card ((a : α) → β a) = Finset.prod Finset.univ fun a => Fintype.card (β a)
@[simp]
theorem Fintype.card_fun {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] :
Fintype.card (αβ) =
@[simp]
theorem card_vector {α : Type u_1} [inst : ] (n : ) :
@[simp]
theorem Finset.sum_attach_univ {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : { a // a Finset.univ }β) :
(Finset.sum (Finset.attach Finset.univ) fun x => f x) = Finset.sum Finset.univ fun x => f { val := x, property := (_ : x Finset.univ) }
@[simp]
theorem Finset.prod_attach_univ {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : { a // a Finset.univ }β) :
(Finset.prod (Finset.attach Finset.univ) fun x => f x) = Finset.prod Finset.univ fun x => f { val := x, property := (_ : x Finset.univ) }
theorem Finset.sum_univ_pi {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] {δ : αType u_3} {t : (a : α) → Finset (δ a)} (f : ((a : α) → a Finset.univδ a) → β) :
(Finset.sum (Finset.pi Finset.univ t) fun x => f x) = Finset.sum () fun x => f fun a x_1 => x a

Taking a sum over univ.pi t is the same as taking the sum over Fintype.piFinset t. univ.pi t and Fintype.piFinset t are essentially the same Finset, but differ in the type of their element, univ.pi t is a Finset (Π a ∈ univ, t a)∈ univ, t a) and Fintype.piFinset t is a Finset (Π a, t a).

theorem Finset.prod_univ_pi {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] {δ : αType u_3} {t : (a : α) → Finset (δ a)} (f : ((a : α) → a Finset.univδ a) → β) :
(Finset.prod (Finset.pi Finset.univ t) fun x => f x) = Finset.prod () fun x => f fun a x_1 => x a

Taking a product over univ.pi t is the same as taking the product over Fintype.piFinset t. univ.pi t and Fintype.piFinset t are essentially the same Finset, but differ in the type of their element, univ.pi t is a Finset (Π a ∈ univ, t a)∈ univ, t a) and Fintype.piFinset t is a Finset (Π a, t a).

theorem Finset.prod_univ_sum {α : Type u_2} {β : Type u_3} [inst : ] [inst : ] [inst : ] {δ : αType u_1} [inst : (a : α) → DecidableEq (δ a)] {t : (a : α) → Finset (δ a)} {f : (a : α) → δ aβ} :
(Finset.prod Finset.univ fun a => Finset.sum (t a) fun b => f a b) = Finset.sum () fun p => Finset.prod Finset.univ fun x => f x (p x)

The product over univ of a sum can be written as a sum over the product of sets, Fintype.piFinset. Finset.prod_sum is an alternative statement when the product is not over univ

theorem Fintype.sum_pow_mul_eq_add_pow (α : Type u_1) [inst : ] {R : Type u_2} [inst : ] (a : R) (b : R) :
(Finset.sum Finset.univ fun s => a ^ * b ^ ()) = (a + b) ^

Summing a^s.card * b^(n-s.card) over all finite subsets s of a fintype of cardinality n gives (a + b)^n. The "good" proof involves expanding along all coordinates using the fact that x^n is multilinear, but multilinear maps are only available now over rings, so we give instead a proof reducing to the usual binomial theorem to have a result over semirings.

theorem Function.Bijective.sum_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ] [inst : ] [inst : ] {f : αβ} (hf : ) (g : βγ) :
(Finset.sum Finset.univ fun i => g (f i)) = Finset.sum Finset.univ fun i => g i
theorem Function.Bijective.prod_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ] [inst : ] [inst : ] {f : αβ} (hf : ) (g : βγ) :
(Finset.prod Finset.univ fun i => g (f i)) = Finset.prod Finset.univ fun i => g i
theorem Equiv.sum_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ] [inst : ] [inst : ] (e : α β) (f : βγ) :
(Finset.sum Finset.univ fun i => f (e i)) = Finset.sum Finset.univ fun i => f i
theorem Equiv.prod_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ] [inst : ] [inst : ] (e : α β) (f : βγ) :
(Finset.prod Finset.univ fun i => f (e i)) = Finset.prod Finset.univ fun i => f i
theorem Equiv.sum_comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ] [inst : ] [inst : ] (e : α β) (f : αγ) (g : βγ) (h : ∀ (i : α), f i = g (e i)) :
(Finset.sum Finset.univ fun i => f i) = Finset.sum Finset.univ fun i => g i
theorem Equiv.prod_comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ] [inst : ] [inst : ] (e : α β) (f : αγ) (g : βγ) (h : ∀ (i : α), f i = g (e i)) :
(Finset.prod Finset.univ fun i => f i) = Finset.prod Finset.univ fun i => g i
theorem Fin.sum_univ_eq_sum_range {α : Type u_1} [inst : ] (f : α) (n : ) :
(Finset.sum Finset.univ fun i => f i) = Finset.sum () fun i => f i

It is equivalent to sum a function over fin n or finset.range n.

theorem Fin.prod_univ_eq_prod_range {α : Type u_1} [inst : ] (f : α) (n : ) :
(Finset.prod Finset.univ fun i => f i) = Finset.prod () fun i => f i

It is equivalent to compute the product of a function over Fin n or Finset.range n.

theorem Finset.sum_fin_eq_sum_range {β : Type u_1} [inst : ] {n : } (c : Fin nβ) :
(Finset.sum Finset.univ fun i => c i) = Finset.sum () fun i => if h : i < n then c { val := i, isLt := h } else 0
theorem Finset.prod_fin_eq_prod_range {β : Type u_1} [inst : ] {n : } (c : Fin nβ) :
(Finset.prod Finset.univ fun i => c i) = Finset.prod () fun i => if h : i < n then c { val := i, isLt := h } else 1
theorem Finset.sum_toFinset_eq_subtype {α : Type u_2} {M : Type u_1} [inst : ] [inst : ] (p : αProp) [inst : ] (f : αM) :
(Finset.sum (Set.toFinset { x | p x }) fun a => f a) = Finset.sum Finset.univ fun a => f a
theorem Finset.prod_toFinset_eq_subtype {α : Type u_2} {M : Type u_1} [inst : ] [inst : ] (p : αProp) [inst : ] (f : αM) :
(Finset.prod (Set.toFinset { x | p x }) fun a => f a) = Finset.prod Finset.univ fun a => f a
theorem Finset.sum_fiberwise {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : ] [inst : ] [inst : ] (s : ) (f : αβ) (g : αγ) :
(Finset.sum Finset.univ fun b => Finset.sum (Finset.filter (fun a => f a = b) s) fun a => g a) = Finset.sum s fun a => g a
theorem Finset.prod_fiberwise {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : ] [inst : ] [inst : ] (s : ) (f : αβ) (g : αγ) :
(Finset.prod Finset.univ fun b => Finset.prod (Finset.filter (fun a => f a = b) s) fun a => g a) = Finset.prod s fun a => g a
theorem Fintype.sum_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ] [inst : ] [inst : ] [inst : ] (f : αβ) (g : αγ) :
(Finset.sum Finset.univ fun b => Finset.sum Finset.univ fun a => g a) = Finset.sum Finset.univ fun a => g a
theorem Fintype.prod_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ] [inst : ] [inst : ] [inst : ] (f : αβ) (g : αγ) :
(Finset.prod Finset.univ fun b => Finset.prod Finset.univ fun a => g a) = Finset.prod Finset.univ fun a => g a
theorem Fintype.prod_dite {α : Type u_1} {β : Type u_2} [inst : ] {p : αProp} [inst : ] [inst : ] (f : (a : α) → p aβ) (g : (a : α) → ¬p aβ) :
(Finset.prod Finset.univ fun a => dite (p a) (f a) (g a)) = (Finset.prod Finset.univ fun a => f (a) a.property) * Finset.prod Finset.univ fun a => g a (_ : ¬p a)
theorem Fintype.sum_sum_elim {α₁ : Type u_2} {α₂ : Type u_3} {M : Type u_1} [inst : Fintype α₁] [inst : Fintype α₂] [inst : ] (f : α₁M) (g : α₂M) :
(Finset.sum Finset.univ fun x => Sum.elim f g x) = (Finset.sum Finset.univ fun a₁ => f a₁) + Finset.sum Finset.univ fun a₂ => g a₂
theorem Fintype.prod_sum_elim {α₁ : Type u_2} {α₂ : Type u_3} {M : Type u_1} [inst : Fintype α₁] [inst : Fintype α₂] [inst : ] (f : α₁M) (g : α₂M) :
(Finset.prod Finset.univ fun x => Sum.elim f g x) = (Finset.prod Finset.univ fun a₁ => f a₁) * Finset.prod Finset.univ fun a₂ => g a₂
@[simp]
theorem Fintype.sum_sum_type {α₁ : Type u_1} {α₂ : Type u_2} {M : Type u_3} [inst : Fintype α₁] [inst : Fintype α₂] [inst : ] (f : α₁ α₂M) :
(Finset.sum Finset.univ fun x => f x) = (Finset.sum Finset.univ fun a₁ => f (Sum.inl a₁)) + Finset.sum Finset.univ fun a₂ => f (Sum.inr a₂)
@[simp]
theorem Fintype.prod_sum_type {α₁ : Type u_1} {α₂ : Type u_2} {M : Type u_3} [inst : Fintype α₁] [inst : Fintype α₂] [inst : ] (f : α₁ α₂M) :
(Finset.prod Finset.univ fun x => f x) = (Finset.prod Finset.univ fun a₁ => f (Sum.inl a₁)) * Finset.prod Finset.univ fun a₂ => f (Sum.inr a₂)