mathlib documentation

data.​fintype.​card

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 → α) :
finset.univ.prod (λ (b : bool), f b) = f bool.tt * f bool.ff

theorem fintype.​sum_bool {α : Type u_1} [add_comm_monoid α] (f : bool → α) :
finset.univ.sum (λ (b : bool), f b) = f bool.tt + f bool.ff

theorem fintype.​card_eq_sum_ones {α : Type u_1} [fintype α] :
fintype.card α = finset.univ.sum (λ (a : α), 1)

theorem fintype.​sum_extend_by_zero {α : Type u_1} {ι : Type u_4} [decidable_eq ι] [fintype ι] [add_comm_monoid α] (s : finset ι) (f : ι → α) :
finset.univ.sum (λ (i : ι), ite (i s) (f i) 0) = s.sum (λ (i : ι), f i)

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

theorem fintype.​sum_eq_zero {α : Type u_1} {M : Type u_4} [fintype α] [add_comm_monoid M] (f : α → M) :
(∀ (a : α), f a = 0)finset.univ.sum (λ (a : α), f a) = 0

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

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

theorem fintype.​sum_congr {α : Type u_1} {M : Type u_4} [fintype α] [add_comm_monoid M] (f g : α → M) :
(∀ (a : α), f a = g a)finset.univ.sum (λ (a : α), f a) = finset.univ.sum (λ (a : α), g a)

theorem fintype.​sum_unique {β : Type u_2} {M : Type u_4} [add_comm_monoid M] [unique β] (f : β → M) :
finset.univ.sum (λ (x : β), f x) = f (inhabited.default β)

theorem fintype.​prod_unique {β : Type u_2} {M : Type u_4} [comm_monoid M] [unique β] (f : β → M) :
finset.univ.prod (λ (x : β), f x) = f (inhabited.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 : s.prod (λ (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.

theorem fintype.​eq_of_subsingleton_of_sum_eq {M : Type u_4} [add_comm_monoid M] {ι : Type u_1} [subsingleton ι] {s : finset ι} {f : ι → M} {b : M} (h : s.sum (λ (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 fin.​prod_univ_succ {β : Type u_2} [comm_monoid β] {n : } (f : fin n.succ → β) :
finset.univ.prod (λ (i : fin n.succ), f i) = f 0 * finset.univ.prod (λ (i : fin n), f i.succ)

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

@[simp]
theorem fin.​sum_univ_zero {β : Type u_2} [add_comm_monoid β] (f : fin 0 → β) :
finset.univ.sum (λ (i : fin 0), f i) = 0

theorem fin.​sum_univ_succ {β : Type u_2} [add_comm_monoid β] {n : } (f : fin n.succ → β) :
finset.univ.sum (λ (i : fin n.succ), f i) = f 0 + finset.univ.sum (λ (i : fin n), f i.succ)

theorem fin.​prod_univ_cast_succ {β : Type u_2} [comm_monoid β] {n : } (f : fin n.succ → β) :
finset.univ.prod (λ (i : fin n.succ), f i) = finset.univ.prod (λ (i : fin n), f i.cast_succ) * f (fin.last n)

theorem fin.​sum_univ_cast_succ {β : Type u_2} [add_comm_monoid β] {n : } (f : fin n.succ → β) :
finset.univ.sum (λ (i : fin n.succ), f i) = finset.univ.sum (λ (i : fin n), f i.cast_succ) + f (fin.last n)

@[simp]
theorem fintype.​card_sigma {α : Type u_1} (β : α → Type u_2) [fintype α] [Π (a : α), fintype (β a)] :
fintype.card (sigma β) = finset.univ.sum (λ (a : α), fintype.card (β a))

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

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

@[simp]
theorem fintype.​card_pi_finset {α : Type u_1} [decidable_eq α] [fintype α] {δ : α → Type u_2} (t : Π (a : α), finset (δ a)) :
(fintype.pi_finset t).card = finset.univ.prod (λ (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) = finset.univ.prod (λ (a : α), fintype.card (β a))

@[simp]
theorem fintype.​card_fun {α : Type u_1} {β : Type u_2} [decidable_eq α] [fintype α] [fintype β] :

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

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

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

theorem finset.​sum_range_eq_sum_fin {β : Type u_2} [add_comm_monoid β] (n : ) (f : → β) :
(finset.range n).sum (λ (k : ), f k) = finset.univ.sum (λ (k : fin n), f k)

theorem finset.​prod_range_eq_prod_fin {β : Type u_2} [comm_monoid β] (n : ) (f : → β) :
(finset.range n).prod (λ (k : ), f k) = finset.univ.prod (λ (k : fin n), f k)

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

theorem finset.​sum_fin_eq_sum_range {β : Type u_2} [add_comm_monoid β] {n : } (c : fin n → β) :
finset.univ.sum (λ (i : fin n), c i) = (finset.range n).sum (λ (i : ), dite (i < n) (λ (h : i < n), c i, h⟩) (λ (h : ¬i < n), 0))

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 finset.univδ a) → β) :
(finset.univ.pi t).prod (λ (x : Π (a : α), a finset.univδ a), f x) = (fintype.pi_finset t).prod (λ (x : Π (a : α), δ a), f (λ (a : α) (_x : a finset.univ), 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 α] [add_comm_monoid β] {δ : α → Type u_3} {t : Π (a : α), finset (δ a)} (f : (Π (a : α), a finset.univδ a) → β) :
(finset.univ.pi t).sum (λ (x : Π (a : α), a finset.univδ a), f x) = (fintype.pi_finset t).sum (λ (x : Π (a : α), δ a), f (λ (a : α) (_x : a finset.univ), 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 α] [comm_semiring β] {δ : α → Type u_1} [Π (a : α), decidable_eq (δ a)] {t : Π (a : α), finset (δ a)} {f : Π (a : α), δ a → β} :
finset.univ.prod (λ (a : α), (t a).sum (λ (b : δ a), f a b)) = (fintype.pi_finset t).sum (λ (p : Π (a : α), δ a), finset.univ.prod (λ (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} [comm_semiring R] (a b : R) :
finset.univ.sum (λ (s : finset α), a ^ s.card * b ^ (fintype.card α - s.card)) = (a + b) ^ fintype.card α

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} [comm_semiring R] (a b : R) :
finset.univ.sum (λ (s : finset (fin n)), a ^ s.card * b ^ (n - s.card)) = (a + b) ^ n

theorem fin.​prod_univ_eq_prod_range {α : Type u_1} [comm_monoid α] (f : → α) (n : ) :
finset.univ.prod (λ (i : fin n), f i.val) = (finset.range n).prod (λ (i : ), f i)

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

theorem fin.​sum_univ_eq_sum_range {α : Type u_1} [add_comm_monoid α] (f : → α) (n : ) :
finset.univ.sum (λ (i : fin n), f i.val) = (finset.range n).sum (λ (i : ), f i)

theorem finset.​sum_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [fintype α] [fintype β] [add_comm_monoid γ] (e : α β) (f : β → γ) :
finset.univ.sum (λ (i : α), f (e i)) = finset.univ.sum (λ (i : β), f i)

theorem finset.​prod_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [fintype α] [fintype β] [comm_monoid γ] (e : α β) (f : β → γ) :
finset.univ.prod (λ (i : α), f (e i)) = finset.univ.prod (λ (i : β), f i)

theorem finset.​sum_subtype {α : Type u_1} {M : Type u_2} [add_comm_monoid M] {p : α → Prop} {F : fintype (subtype p)} {s : finset α} (h : ∀ (x : α), x s p x) (f : α → M) :
s.sum (λ (a : α), f a) = finset.univ.sum (λ (a : subtype p), f a)

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) :
s.prod (λ (a : α), f a) = finset.univ.prod (λ (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 : α → γ) :
finset.univ.prod (λ (b : β), (finset.filter (λ (a : α), f a = b) s).prod (λ (a : α), g a)) = s.prod (λ (a : α), g a)

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

theorem fintype.​sum_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [fintype α] [decidable_eq β] [fintype β] [add_comm_monoid γ] (f : α → β) (g : α → γ) :
finset.univ.sum (λ (b : β), finset.univ.sum (λ (a : {a // f a = b}), g a)) = finset.univ.sum (λ (a : α), g a)

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

theorem fintype.​sum_sum_type {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [fintype α₁] [fintype α₂] [add_comm_monoid M] (f : α₁ α₂ → M) :
finset.univ.sum (λ (x : α₁ α₂), f x) = finset.univ.sum (λ (a₁ : α₁), f (sum.inl a₁)) + finset.univ.sum (λ (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) :
finset.univ.prod (λ (x : α₁ α₂), f x) = finset.univ.prod (λ (a₁ : α₁), f (sum.inl a₁)) * finset.univ.prod (λ (a₂ : α₂), f (sum.inr a₂))

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

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

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

theorem list.​sum_of_fn {α : Type u_1} [add_comm_monoid α] {n : } {f : fin n → α} :
(list.of_fn f).sum = finset.univ.sum (λ (i : fin n), f i)

theorem list.​alternating_sum_eq_finset_sum {G : Type u_1} [add_comm_group G] (L : list G) :

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