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} [AddCommMonoid α] (f : Bool → α) : ∑ b : Bool, f b = f true + f false

theorem Fintype.prod_bool {α : Type u_1} [CommMonoid α] (f : Bool → α) : ∏ b : Bool, f b = f true * f false

theorem Fintype.card_eq_sum_ones {α : Type u_4} [Fintype α] : Fintype.card α = ∑ _a : α, 1

theorem Fintype.sum_extend_by_zero {α : Type u_1} {ι : Type u_4} [DecidableEq ι] [Fintype ι] [AddCommMonoid α] (s : Finset ι) (f : ι → α) : (∑ i : ι, if i ∈ s then f i else 0) = ∑ i ∈ s, f i

theorem Fintype.prod_extend_by_one {α : Type u_1} {ι : Type u_4} [DecidableEq ι] [Fintype ι] [CommMonoid α] (s : Finset ι) (f : ι → α) : (∏ i : ι, if i ∈ s then f i else 1) = ∏ i ∈ s, f i

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

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

theorem Fintype.sum_congr {α : Type u_1} {M : Type u_4} [Fintype α] [AddCommMonoid M] (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} [Fintype α] [CommMonoid M] (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} [Fintype α] [AddCommMonoid M] {f : α → M} (a : α) (h : ∀ (x : α), x ≠ a → f x = 0) : ∑ x : α, f x = f a

theorem Fintype.prod_eq_single {α : Type u_1} {M : Type u_4} [Fintype α] [CommMonoid M] {f : α → M} (a : α) (h : ∀ (x : α), x ≠ a → f x = 1) : ∏ x : α, f x = f a

theorem Fintype.sum_eq_add {α : Type u_1} {M : Type u_4} [Fintype α] [AddCommMonoid M] {f : α → M} (a : α) (b : α) (h₁ : a ≠ b) (h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 0) : ∑ x : α, f x = f a + f b

theorem Fintype.prod_eq_mul {α : Type u_1} {M : Type u_4} [Fintype α] [CommMonoid M] {f : α → M} (a : α) (b : α) (h₁ : a ≠ b) (h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1) : ∏ x : α, f x = f a * f b

theorem Fintype.eq_of_subsingleton_of_sum_eq {M : Type u_4} [AddCommMonoid M] {ι : Type u_5} [Subsingleton ι] {s : Finset ι} {f : ι → M} {b : M} (h : ∑ i ∈ s, f i = b) (i : ι) : i ∈ s → f 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} [CommMonoid M] {ι : Type u_5} [Subsingleton ι] {s : Finset ι} {f : ι → M} {b : M} (h : ∏ i ∈ s, f i = b) (i : ι) : i ∈ s → f 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} [Fintype α] [AddCommMonoid M] (f : Option α → M) : ∑ i : Option α, f i = f none + ∑ i : α, f (some i)

@[simp]

theorem Fintype.prod_option {α : Type u_1} {M : Type u_4} [Fintype α] [CommMonoid M] (f : Option α → M) : ∏ i : Option α, f i = f none * ∏ i : α, f (some i)

@[simp]

theorem Finset.card_pi {ι : Type u_4} {α : ι → Type u_6} [DecidableEq ι] (s : Finset ι) (t : (i : ι) → Finset (α i)) : (s.pi t).card = ∏ i ∈ s, (t i).card

@[simp]

theorem Fintype.card_piFinset {ι : Type u_4} {α : ι → Type u_6} [DecidableEq ι] [Fintype ι] (s : (i : ι) → Finset (α i)) : (Fintype.piFinset s).card = ∏ i : ι, (s i).card

theorem Fintype.card_piFinset_const {α : Type u_7} (s : Finset α) (n : ℕ) : (Fintype.piFinset fun (x : Fin n) => s).card = s.card ^ n

This lemma is specifically designed to be used backwards, whence the specialisation to Fin n as the indexing type doesn't matter in practice. The more general forward direction lemma here is Fintype.card_piFinset.

@[simp]

theorem Fintype.card_pi {ι : Type u_4} {α : ι → Type u_6} [DecidableEq ι] [Fintype ι] [(i : ι) → Fintype (α i)] : Fintype.card ((i : ι) → α i) = ∏ i : ι, Fintype.card (α i)

theorem Fintype.card_pi_const (α : Type u_7) [Fintype α] (n : ℕ) : Fintype.card (Fin n → α) = Fintype.card α ^ n

This lemma is specifically designed to be used backwards, whence the specialisation to Fin n as the indexing type doesn't matter in practice. The more general forward direction lemma here is Fintype.card_pi.

@[simp]

theorem Fintype.card_sigma {ι : Type u_8} {α : ι → Type u_7} [Fintype ι] [(i : ι) → Fintype (α i)] : Fintype.card (Sigma α) = ∑ i : ι, Fintype.card (α i)

theorem Fintype.card_filter_piFinset_eq_of_mem {ι : Type u_4} {α : ι → Type u_6} [DecidableEq ι] [Fintype ι] [(i : ι) → DecidableEq (α i)] (s : (i : ι) → Finset (α i)) (i : ι) {a : α i} (ha : a ∈ s i) : (Finset.filter (fun (f : (a : ι) → α a) => f i = a) (Fintype.piFinset s)).card = ∏ j ∈ Finset.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} [DecidableEq ι] [DecidableEq κ] [Fintype ι] (s : Finset κ) (i : ι) {x : κ} (hx : x ∈ s) : (Finset.filter (fun (f : ι → κ) => f i = x) (Fintype.piFinset fun (x : ι) => s)).card = s.card ^ (Fintype.card ι - 1)

theorem Fintype.card_filter_piFinset_eq {ι : Type u_4} {α : ι → Type u_6} [DecidableEq ι] [Fintype ι] [(i : ι) → DecidableEq (α i)] (s : (i : ι) → Finset (α i)) (i : ι) (a : α i) : (Finset.filter (fun (f : (a : ι) → α a) => f i = a) (Fintype.piFinset s)).card = if a ∈ s i then ∏ b ∈ Finset.univ.erase i, (s b).card else 0

theorem Fintype.card_filter_piFinset_const {ι : Type u_4} {κ : Type u_5} [DecidableEq ι] [DecidableEq κ] [Fintype ι] (s : Finset κ) (i : ι) (j : κ) : (Finset.filter (fun (f : ι → κ) => f i = j) (Fintype.piFinset fun (x : ι) => s)).card = if j ∈ s then s.card ^ (Fintype.card ι - 1) else 0

theorem Fintype.card_fun {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] : Fintype.card (α → β) = Fintype.card β ^ Fintype.card α

@[simp]

theorem card_vector {α : Type u_1} [Fintype α] (n : ℕ) : Fintype.card (Mathlib.Vector α n) = Fintype.card α ^ n

theorem Fin.sum_univ_eq_sum_range {α : Type u_1} [AddCommMonoid α] (f : ℕ → α) (n : ℕ) : ∑ i : Fin n, f ↑i = ∑ i ∈ Finset.range n, 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} [CommMonoid α] (f : ℕ → α) (n : ℕ) : ∏ i : Fin n, f ↑i = ∏ i ∈ Finset.range n, 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} [AddCommMonoid β] {n : ℕ} (c : Fin n → β) : ∑ i : Fin n, c i = ∑ i ∈ Finset.range n, if h : i < n then c ⟨i, h⟩ else 0

theorem Finset.prod_fin_eq_prod_range {β : Type u_2} [CommMonoid β] {n : ℕ} (c : Fin n → β) : ∏ i : Fin n, c i = ∏ i ∈ Finset.range n, if h : i < n then c ⟨i, h⟩ else 1

theorem Finset.sum_toFinset_eq_subtype {α : Type u_1} {M : Type u_4} [AddCommMonoid M] [Fintype α] (p : α → Prop) [DecidablePred p] (f : α → M) : ∑ a ∈ {x : α | p x}.toFinset, f a = ∑ a : Subtype p, f ↑a

theorem Finset.prod_toFinset_eq_subtype {α : Type u_1} {M : Type u_4} [CommMonoid M] [Fintype α] (p : α → Prop) [DecidablePred p] (f : α → M) : ∏ a ∈ {x : α | p x}.toFinset, f a = ∏ a : Subtype p, f ↑a

theorem Fintype.prod_dite {α : Type u_1} {β : Type u_2} [Fintype α] {p : α → Prop} [DecidablePred p] [CommMonoid β] (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 α₂] [AddCommMonoid M] (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 α₂] [CommMonoid M] (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 α₂] [AddCommMonoid M] (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 α₂] [CommMonoid M] (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 α₂] [AddCommMonoid γ] {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 α₂] [CommMonoid γ] {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 α₂] [AddCommMonoid γ] {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 α₂] [CommMonoid γ] {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 α₂] [AddCommMonoid γ] {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 α₂] [CommMonoid γ] {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 α₂] [AddCommMonoid γ] {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 α₂] [CommMonoid γ] {f : α₁ → α₂ → γ} : ∏ x : α₁ × α₂, f x.1 x.2 = ∏ y : α₂, ∏ x : α₁, f x y

An uncurried version of Finset.prod_prod_type_right.