# 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.Group.Finset and should be moved at some point.

theorem Fintype.sum_bool {α : Type u_1} [] (f : Boolα) :
b : Bool, f b = f true +
theorem Fintype.prod_bool {α : Type u_1} [] (f : Boolα) :
b : Bool, f b = f true *
theorem Fintype.card_eq_sum_ones {α : Type u_4} [] :
= _a : α, 1
theorem Fintype.sum_extend_by_zero {α : Type u_1} {ι : Type u_4} [] [] [] (s : ) (f : ια) :
(i : ι, if i s then f i else 0) = is, f i
theorem Fintype.prod_extend_by_one {α : Type u_1} {ι : Type u_4} [] [] [] (s : ) (f : ια) :
(i : ι, if i s then f i else 1) = is, f i
theorem Fintype.sum_eq_zero {α : Type u_1} {M : Type u_4} [] [] (f : αM) (h : ∀ (a : α), f a = 0) :
a : α, f a = 0
theorem Fintype.prod_eq_one {α : Type u_1} {M : Type u_4} [] [] (f : αM) (h : ∀ (a : α), f a = 1) :
a : α, f a = 1
theorem Fintype.sum_congr {α : Type u_1} {M : Type u_4} [] [] (f : αM) (g : αM) (h : ∀ (a : α), f a = g a) :
a : α, f a = a : α, g a
theorem Fintype.prod_congr {α : Type u_1} {M : Type u_4} [] [] (f : αM) (g : αM) (h : ∀ (a : α), f a = g a) :
a : α, f a = a : α, g a
theorem Fintype.sum_eq_single {α : Type u_1} {M : Type u_4} [] [] {f : αM} (a : α) (h : ∀ (x : α), x af x = 0) :
x : α, f x = f a
theorem Fintype.prod_eq_single {α : Type u_1} {M : Type u_4} [] [] {f : αM} (a : α) (h : ∀ (x : α), x af x = 1) :
x : α, f x = f a
theorem Fintype.sum_eq_add {α : Type u_1} {M : Type u_4} [] [] {f : αM} (a : α) (b : α) (h₁ : a b) (h₂ : ∀ (x : α), x a x bf x = 0) :
x : α, f x = f a + f b
theorem Fintype.prod_eq_mul {α : Type u_1} {M : Type u_4} [] [] {f : αM} (a : α) (b : α) (h₁ : a b) (h₂ : ∀ (x : α), x a x bf x = 1) :
x : α, f x = f a * f b
theorem Fintype.eq_of_subsingleton_of_sum_eq {M : Type u_4} [] {ι : Type u_5} [] {s : } {f : ιM} {b : M} (h : is, 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_4} [] {ι : Type u_5} [] {s : } {f : ιM} {b : M} (h : is, 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_4} [] [] (f : M) :
i : , f i = f none + i : α, f (some i)
@[simp]
theorem Fintype.prod_option {α : Type u_1} {M : Type u_4} [] [] (f : M) :
i : , f i = f none * i : α, f (some i)
@[simp]
theorem Finset.card_pi {ι : Type u_4} {α : ιType u_6} [] (s : ) (t : (i : ι) → Finset (α i)) :
(s.pi t).card = is, (t i).card
@[simp]
theorem Fintype.card_piFinset {ι : Type u_4} {α : ιType u_6} [] [] (s : (i : ι) → Finset (α i)) :
().card = i : ι, (s i).card
@[simp]
theorem Fintype.card_pi {ι : Type u_4} {α : ιType u_6} [] [] [(i : ι) → Fintype (α i)] :
Fintype.card ((i : ι) → α i) = i : ι, Fintype.card (α i)
@[simp]
theorem Fintype.card_sigma {ι : Type u_4} {α : ιType u_6} [] [(i : ι) → Fintype (α i)] :
= i : ι, Fintype.card (α i)
theorem Fintype.card_filter_piFinset_eq_of_mem {ι : Type u_4} {α : ιType u_6} [] [] [(i : ι) → DecidableEq (α i)] (s : (i : ι) → Finset (α i)) (i : ι) {a : α i} (ha : a s i) :
(Finset.filter (fun (f : (a : ι) → α a) => f i = a) ()).card = jFinset.univ.erase i, (s j).card

The number of dependent maps f : Π j, s j for which the i component is a is the product over all j ≠ i of (s j).card.

Note that this is just a composition of easier lemmas, but there's some glue missing to make that smooth enough not to need this lemma.

theorem Fintype.card_filter_piFinset_const_eq_of_mem {ι : Type u_4} {κ : Type u_5} [] [] [] (s : ) (i : ι) {x : κ} (hx : x s) :
(Finset.filter (fun (f : ικ) => f i = x) (Fintype.piFinset fun (x : ι) => s)).card = s.card ^ ()
theorem Fintype.card_filter_piFinset_eq {ι : Type u_4} {α : ιType u_6} [] [] [(i : ι) → DecidableEq (α i)] (s : (i : ι) → Finset (α i)) (i : ι) (a : α i) :
(Finset.filter (fun (f : (a : ι) → α a) => f i = a) ()).card = if a s i then bFinset.univ.erase i, (s b).card else 0
theorem Fintype.card_filter_piFinset_const {ι : Type u_4} {κ : Type u_5} [] [] [] (s : ) (i : ι) (j : κ) :
(Finset.filter (fun (f : ικ) => f i = j) (Fintype.piFinset fun (x : ι) => s)).card = if j s then s.card ^ () else 0
theorem Fintype.card_fun {α : Type u_1} {β : Type u_2} [] [] [] :
Fintype.card (αβ) =
@[simp]
theorem card_vector {α : Type u_1} [] (n : ) :
theorem Fin.sum_univ_eq_sum_range {α : Type u_1} [] (f : α) (n : ) :
i : Fin n, f i = 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} [] (f : α) (n : ) :
i : Fin n, f i = 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_2} [] {n : } (c : Fin nβ) :
i : Fin n, c i = i, if h : i < n then c i, h else 0
theorem Finset.prod_fin_eq_prod_range {β : Type u_2} [] {n : } (c : Fin nβ) :
i : Fin n, c i = i, if h : i < n then c i, h else 1
theorem Finset.sum_toFinset_eq_subtype {α : Type u_1} {M : Type u_4} [] [] (p : αProp) [] (f : αM) :
a{x : α | p x}.toFinset, f a = a : , f a
theorem Finset.prod_toFinset_eq_subtype {α : Type u_1} {M : Type u_4} [] [] (p : αProp) [] (f : αM) :
a{x : α | p x}.toFinset, f a = a : , f a
theorem Fintype.prod_dite {α : Type u_1} {β : Type u_2} [] {p : αProp} [] [] (f : (a : α) → p aβ) (g : (a : α) → ¬p aβ) :
a : α, dite (p a) (f a) (g a) = (a : { a : α // p a }, f a ) * a : { a : α // ¬p a }, g a
theorem Fintype.sum_sum_elim {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [Fintype α₁] [Fintype α₂] [] (f : α₁M) (g : α₂M) :
x : α₁ α₂, Sum.elim f g x = a₁ : α₁, f a₁ + a₂ : α₂, g a₂
theorem Fintype.prod_sum_elim {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [Fintype α₁] [Fintype α₂] [] (f : α₁M) (g : α₂M) :
x : α₁ α₂, Sum.elim f g x = (a₁ : α₁, f a₁) * a₂ : α₂, g a₂
@[simp]
theorem Fintype.sum_sum_type {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [Fintype α₁] [Fintype α₂] [] (f : α₁ α₂M) :
x : α₁ α₂, f x = a₁ : α₁, f (Sum.inl a₁) + a₂ : α₂, f (Sum.inr a₂)
@[simp]
theorem Fintype.prod_sum_type {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [Fintype α₁] [Fintype α₂] [] (f : α₁ α₂M) :
x : α₁ α₂, f x = (a₁ : α₁, f (Sum.inl a₁)) * a₂ : α₂, f (Sum.inr a₂)
@[simp]
theorem Fintype.sum_prod_type {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [] {f : α₁ × α₂γ} :
x : α₁ × α₂, f x = x : α₁, y : α₂, f (x, y)
@[simp]
theorem Fintype.prod_prod_type {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [] {f : α₁ × α₂γ} :
x : α₁ × α₂, f x = x : α₁, y : α₂, f (x, y)
theorem Fintype.sum_prod_type' {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [] {f : α₁α₂γ} :
x : α₁ × α₂, f x.1 x.2 = x : α₁, y : α₂, f x y

An uncurried version of Finset.sum_prod_type

theorem Fintype.prod_prod_type' {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [] {f : α₁α₂γ} :
x : α₁ × α₂, f x.1 x.2 = x : α₁, y : α₂, f x y

An uncurried version of Finset.prod_prod_type.

theorem Fintype.sum_prod_type_right {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [] {f : α₁ × α₂γ} :
x : α₁ × α₂, f x = y : α₂, x : α₁, f (x, y)
theorem Fintype.prod_prod_type_right {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [] {f : α₁ × α₂γ} :
x : α₁ × α₂, f x = y : α₂, x : α₁, f (x, y)
theorem Fintype.sum_prod_type_right' {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [] {f : α₁α₂γ} :
x : α₁ × α₂, f x.1 x.2 = y : α₂, x : α₁, f x y

An uncurried version of Finset.sum_prod_type_right

theorem Fintype.prod_prod_type_right' {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [] {f : α₁α₂γ} :
x : α₁ × α₂, f x.1 x.2 = y : α₂, x : α₁, f x y

An uncurried version of Finset.prod_prod_type_right.