# mathlibdocumentation

data.fintype.card

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, but was moved here to avoid requiring algebra.big_operators (and hence many other imports) as a dependency of fintype.

theorem fintype.prod_bool {α : Type u_1} [comm_monoid α] (f : bool → α) :
∏ (b : bool), f b = (f tt) * f ff

theorem fintype.sum_bool {α : Type u_1} (f : bool → α) :
∑ (b : bool), f b = f tt + f ff

theorem fintype.card_eq_sum_ones {α : Type u_1} [fintype α] :
= ∑ (a : α), 1

theorem fintype.prod_extend_by_one {α : Type u_1} {ι : Type u_4} [decidable_eq ι] [fintype ι] [comm_monoid α] (s : finset ι) (f : ι → α) :
∏ (i : ι), ite (i s) (f i) 1 = ∏ (i : ι) in s, f i

theorem fintype.sum_extend_by_zero {α : Type u_1} {ι : Type u_4} [decidable_eq ι] [fintype ι] (s : finset ι) (f : ι → α) :
∑ (i : ι), ite (i s) (f i) 0 = ∑ (i : ι) in s, f i

theorem fintype.prod_eq_one {α : Type u_1} {M : Type u_4} [fintype α] [comm_monoid M] (f : α → M) :
(∀ (a : α), f a = 1)∏ (a : α), f a = 1

theorem fintype.sum_eq_zero {α : Type u_1} {M : Type u_4} [fintype α] (f : α → M) :
(∀ (a : α), f a = 0)∑ (a : α), f a = 0

theorem fintype.prod_congr {α : Type u_1} {M : Type u_4} [fintype α] [comm_monoid M] (f g : α → M) :
(∀ (a : α), f a = g a)∏ (a : α), f a = ∏ (a : α), g a

theorem fintype.sum_congr {α : Type u_1} {M : Type u_4} [fintype α] (f g : α → M) :
(∀ (a : α), f a = g a)∑ (a : α), f a = ∑ (a : α), g a

theorem fintype.sum_unique {β : Type u_2} {M : Type u_4} [unique β] (f : β → M) :
∑ (x : β), f x = f (default β)

theorem fintype.prod_unique {β : Type u_2} {M : Type u_4} [comm_monoid M] [unique β] (f : β → M) :
∏ (x : β), f x = f (default β)

theorem fintype.eq_of_subsingleton_of_prod_eq {M : Type u_4} [comm_monoid M] {ι : Type u_1} [subsingleton ι] {s : finset ι} {f : ι → M} {b : M} (h : ∏ (i : ι) in s, 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.

theorem fintype.eq_of_subsingleton_of_sum_eq {M : Type u_4} {ι : Type u_1} [subsingleton ι] {s : finset ι} {f : ι → M} {b : M} (h : ∑ (i : ι) in s, 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 fin.prod_univ_def {β : Type u_2} [comm_monoid β] {n : } (f : fin n → β) :
∏ (i : fin n), f i = (list.map f (list.fin_range n)).prod

theorem fin.sum_univ_def {β : Type u_2} {n : } (f : fin n → β) :
∑ (i : fin n), f i = (list.map f (list.fin_range n)).sum

theorem fin.sum_of_fn {β : Type u_2} {n : } (f : fin n → β) :
(list.of_fn f).sum = ∑ (i : fin n), f i

theorem fin.prod_of_fn {β : Type u_2} [comm_monoid β] {n : } (f : fin n → β) :
(list.of_fn f).prod = ∏ (i : fin n), f i

@[simp]
theorem fin.sum_univ_zero {β : Type u_2} (f : fin 0 → β) :
∑ (i : fin 0), f i = 0

A sum of a function f : fin 0 → β is 0 because fin 0 is empty

@[simp]
theorem fin.prod_univ_zero {β : Type u_2} [comm_monoid β] (f : fin 0 → β) :
∏ (i : fin 0), f i = 1

A product of a function f : fin 0 → β is 1 because fin 0 is empty

theorem fin.prod_univ_succ_above {β : Type u_2} [comm_monoid β] {n : } (f : fin (n + 1) → β) (x : fin (n + 1)) :
∏ (i : fin (n + 1)), f i = (f x) * ∏ (i : fin n), f (x.succ_above i)

A product of a function f : fin (n + 1) → β over all fin (n + 1) is the product of f x, for some x : fin (n + 1) times the remaining product

theorem fin.sum_univ_succ_above {β : Type u_2} {n : } (f : fin (n + 1) → β) (x : fin (n + 1)) :
∑ (i : fin (n + 1)), f i = f x + ∑ (i : fin n), f (x.succ_above i)

A sum of a function f : fin (n + 1) → β over all fin (n + 1) is the sum of f x, for some x : fin (n + 1) plus the remaining product

theorem fin.prod_univ_succ {β : Type u_2} [comm_monoid β] {n : } (f : fin (n + 1) → β) :
∏ (i : fin (n + 1)), f i = (f 0) * ∏ (i : fin n), f i.succ

A product of a function f : fin (n + 1) → β over all fin (n + 1) is the product of f 0 plus the remaining product

theorem fin.sum_univ_succ {β : Type u_2} {n : } (f : fin (n + 1) → β) :
∑ (i : fin (n + 1)), f i = f 0 + ∑ (i : fin n), f i.succ

A sum of a function f : fin (n + 1) → β over all fin (n + 1) is the sum of f 0 plus the remaining product

theorem fin.prod_univ_cast_succ {β : Type u_2} [comm_monoid β] {n : } (f : fin (n + 1) → β) :
∏ (i : fin (n + 1)), f i = (∏ (i : fin n), f i.cast_succ) * f (fin.last n)

A product of a function f : fin (n + 1) → β over all fin (n + 1) is the product of f (fin.last n) plus the remaining product

theorem fin.sum_univ_cast_succ {β : Type u_2} {n : } (f : fin (n + 1) → β) :
∑ (i : fin (n + 1)), f i = ∑ (i : fin n), f i.cast_succ + f (fin.last n)

A sum of a function f : fin (n + 1) → β over all fin (n + 1) is the sum of f (fin.last n) plus the remaining sum

@[simp]
theorem fintype.card_sigma {α : Type u_1} (β : α → Type u_2) [fintype α] [Π (a : α), fintype (β a)] :
= ∑ (a : α), fintype.card (β a)

@[simp]
theorem fintype.card_sum (α : Type u_1) (β : Type u_2) [fintype α] [fintype β] :
fintype.card β) =

@[simp]
theorem finset.card_pi {α : Type u_1} [decidable_eq α] {δ : α → Type u_2} (s : finset α) (t : Π (a : α), finset (δ a)) :
(s.pi t).card = ∏ (a : α) in s, (t a).card

@[simp]
theorem fintype.card_pi_finset {α : Type u_1} [decidable_eq α] [fintype α] {δ : α → Type u_2} (t : Π (a : α), finset (δ a)) :
= ∏ (a : α), (t a).card

@[simp]
theorem fintype.card_pi {α : Type u_1} {β : α → Type u_2} [decidable_eq α] [fintype α] [f : Π (a : α), fintype (β a)] :
fintype.card (Π (a : α), β a) = ∏ (a : α), fintype.card (β a)

@[simp]
theorem fintype.card_fun {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype α] [fintype β] :
fintype.card (α → β) =

@[simp]
theorem card_vector {α : Type u_1} [fintype α] (n : ) :

@[simp]
theorem finset.prod_attach_univ {α : Type u_1} {β : Type u_2} [fintype α] [comm_monoid β] (f : {a // → β) :
∏ (x : {x // x finset.univ}) in finset.univ.attach, f x = ∏ (x : α), f x, _⟩

@[simp]
theorem finset.sum_attach_univ {α : Type u_1} {β : Type u_2} [fintype α] (f : {a // → β) :
∑ (x : {x // x finset.univ}) in finset.univ.attach, f x = ∑ (x : α), f x, _⟩

theorem finset.prod_univ_pi {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype α] [comm_monoid β] {δ : α → Type u_3} {t : Π (a : α), finset (δ a)} (f : (Π (a : α), δ a) → β) :
∏ (x : Π (a : α), δ a) in , f x = ∏ (x : Π (a : α), δ a) in , f (λ (a : α) (_x : , x a)

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

theorem finset.sum_univ_pi {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype α] {δ : α → Type u_3} {t : Π (a : α), finset (δ a)} (f : (Π (a : α), δ a) → β) :
∑ (x : Π (a : α), δ a) in , f x = ∑ (x : Π (a : α), δ a) in , f (λ (a : α) (_x : , x a)

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

theorem finset.prod_univ_sum {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype α] {δ : α → Type u_1} [Π (a : α), decidable_eq (δ a)] {t : Π (a : α), finset (δ a)} {f : Π (a : α), δ a → β} :
∏ (a : α), ∑ (b : δ a) in t a, f a b = ∑ (p : Π (a : α), δ a) in , ∏ (x : α), f x (p x)

The product over univ of a sum can be written as a sum over the product of sets, fintype.pi_finset. 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) [fintype α] {R : Type u_2} (a b : R) :
∑ (s : finset α), (a ^ s.card) * b ^ - s.card) = (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 fin.sum_pow_mul_eq_add_pow {n : } {R : Type u_1} (a b : R) :
∑ (s : finset (fin n)), (a ^ s.card) * b ^ (n - s.card) = (a + b) ^ n

theorem equiv.sum_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [fintype α] [fintype β] (e : α β) (f : β → γ) :
∑ (i : α), f (e i) = ∑ (i : β), f i

theorem equiv.prod_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [fintype α] [fintype β] [comm_monoid γ] (e : α β) (f : β → γ) :
∏ (i : α), f (e i) = ∏ (i : β), f i

theorem fin.sum_univ_eq_sum_range {α : Type u_1} (f : → α) (n : ) :
∑ (i : fin n), f i = ∑ (i : ) in , f i

theorem fin.prod_univ_eq_prod_range {α : Type u_1} [comm_monoid α] (f : → α) (n : ) :
∏ (i : fin n), f i = ∏ (i : ) in , f i

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

theorem finset.prod_fin_eq_prod_range {β : Type u_2} [comm_monoid β] {n : } (c : fin n → β) :
∏ (i : fin n), c i = ∏ (i : ) in , dite (i < n) (λ (h : i < n), c i, h⟩) (λ (h : ¬i < n), 1)

theorem finset.sum_fin_eq_sum_range {β : Type u_2} {n : } (c : fin n → β) :
∑ (i : fin n), c i = ∑ (i : ) in , dite (i < n) (λ (h : i < n), c i, h⟩) (λ (h : ¬i < n), 0)

theorem finset.prod_subtype {α : Type u_1} {M : Type u_2} [comm_monoid M] {p : α → Prop} {F : fintype (subtype p)} {s : finset α} (h : ∀ (x : α), x s p x) (f : α → M) :
∏ (a : α) in s, f a = ∏ (a : subtype p), f a

theorem finset.sum_subtype {α : Type u_1} {M : Type u_2} {p : α → Prop} {F : fintype (subtype p)} {s : finset α} (h : ∀ (x : α), x s p x) (f : α → M) :
∑ (a : α) in s, f a = ∑ (a : subtype p), f a

theorem finset.prod_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq β] [fintype β] [comm_monoid γ] (s : finset α) (f : α → β) (g : α → γ) :
∏ (b : β), ∏ (a : α) in finset.filter (λ (a : α), f a = b) s, g a = ∏ (a : α) in s, g a

theorem finset.sum_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq β] [fintype β] (s : finset α) (f : α → β) (g : α → γ) :
∑ (b : β), ∑ (a : α) in finset.filter (λ (a : α), f a = b) s, g a = ∑ (a : α) in s, g a

theorem fintype.sum_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [fintype α] [decidable_eq β] [fintype β] (f : α → β) (g : α → γ) :
∑ (b : β) (a : {a // f a = b}), g a = ∑ (a : α), g a

theorem fintype.prod_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [fintype α] [decidable_eq β] [fintype β] [comm_monoid γ] (f : α → β) (g : α → γ) :
∏ (b : β) (a : {a // f a = b}), g a = ∏ (a : α), g a

theorem fintype.prod_dite {α : Type u_1} {β : Type u_2} [fintype α] {p : α → Prop} [comm_monoid β] (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_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₂)

theorem fintype.prod_sum_type {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [fintype α₁] [fintype α₂] [comm_monoid M] (f : α₁ α₂ → M) :
∏ (x : α₁ α₂), f x = (∏ (a₁ : α₁), f (sum.inl a₁)) * ∏ (a₂ : α₂), f (sum.inr a₂)

theorem list.prod_take_of_fn {α : Type u_1} [comm_monoid α] {n : } (f : fin n → α) (i : ) :
(list.of_fn f)).prod = ∏ (j : fin n) in finset.filter (λ (j : fin n), j.val < i) finset.univ, f j

theorem list.sum_take_of_fn {α : Type u_1} {n : } (f : fin n → α) (i : ) :
(list.of_fn f)).sum = ∑ (j : fin n) in finset.filter (λ (j : fin n), j.val < i) finset.univ, f j

theorem list.sum_of_fn {α : Type u_1} {n : } {f : fin n → α} :
(list.of_fn f).sum = ∑ (i : fin n), f i

theorem list.prod_of_fn {α : Type u_1} [comm_monoid α] {n : } {f : fin n → α} :
(list.of_fn f).prod = ∏ (i : fin n), f i

theorem list.alternating_sum_eq_finset_sum {G : Type u_1} (L : list G) :
L.alternating_sum = ∑ (i : fin L.length), (-1) ^ i •ℤ L.nth_le i _

theorem list.alternating_prod_eq_finset_prod {G : Type u_1} [comm_group G] (L : list G) :
L.alternating_prod = ∏ (i : fin L.length), L.nth_le i _ ^ (-1) ^ i