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} [AddCommMonoid α] (f : Bool → α) : (Finset.sum Finset.univ fun (b : Bool) => f b) = f true + f false

theorem Fintype.prod_bool {α : Type u_1} [CommMonoid α] (f : Bool → α) : (Finset.prod Finset.univ fun (b : Bool) => f b) = f true * f false

theorem Fintype.card_eq_sum_ones {α : Type u_4} [Fintype α] : Fintype.card α = Finset.sum Finset.univ fun (_a : α) => 1

theorem Fintype.sum_extend_by_zero {α : Type u_1} {ι : Type u_4} [DecidableEq ι] [Fintype ι] [AddCommMonoid α] (s : Finset ι) (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_4} [DecidableEq ι] [Fintype ι] [CommMonoid α] (s : Finset ι) (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_1} {M : Type u_4} [Fintype α] [AddCommMonoid M] (f : α → M) (h : ∀ (a : α), f a = 0) : (Finset.sum Finset.univ fun (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) : (Finset.prod Finset.univ fun (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) : (Finset.sum Finset.univ fun (a : α) => f a) = Finset.sum Finset.univ fun (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) : (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_4} [Fintype α] [AddCommMonoid M] {f : α → M} (a : α) (h : ∀ (x : α), x ≠ a → f x = 0) : (Finset.sum Finset.univ fun (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) : (Finset.prod Finset.univ fun (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) : (Finset.sum Finset.univ fun (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) : (Finset.prod Finset.univ fun (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 : (Finset.sum s fun (i : ι) => 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 : (Finset.prod s fun (i : ι) => 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) : (Finset.sum Finset.univ fun (i : Option α) => f i) = f none + Finset.sum Finset.univ fun (i : α) => f (some i)

@[simp]

theorem Fintype.prod_option {α : Type u_1} {M : Type u_4} [Fintype α] [CommMonoid M] (f : Option α → M) : (Finset.prod Finset.univ fun (i : Option α) => f i) = f none * Finset.prod Finset.univ fun (i : α) => f (some i)

@[simp]

theorem Fintype.card_sigma {α : Type u_4} (β : α → Type u_5) [Fintype α] [(a : α) → Fintype (β a)] : Fintype.card (Sigma β) = Finset.sum Finset.univ fun (a : α) => Fintype.card (β a)

@[simp]

theorem Finset.card_pi {α : Type u_1} [DecidableEq α] {δ : α → Type u_4} (s : Finset α) (t : (a : α) → Finset (δ a)) : Finset.card (Finset.pi s t) = Finset.prod s fun (a : α) => Finset.card (t a)

@[simp]

theorem Fintype.card_piFinset {α : Type u_1} [DecidableEq α] [Fintype α] {δ : α → Type u_4} (t : (a : α) → Finset (δ a)) : Finset.card (Fintype.piFinset t) = Finset.prod Finset.univ fun (a : α) => Finset.card (t a)

@[simp]

theorem Fintype.card_pi {α : Type u_1} {β : α → Type u_4} [DecidableEq α] [Fintype α] [(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} [DecidableEq α] [Fintype α] [Fintype β] : Fintype.card (α → β) = Fintype.card β ^ Fintype.card α

@[simp]

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

@[simp]

theorem Finset.sum_attach_univ {α : Type u_1} {β : Type u_2} [Fintype α] [AddCommMonoid β] (f : { a : α // a ∈ Finset.univ } → β) : (Finset.sum (Finset.attach Finset.univ) fun (x : { x : α // x ∈ Finset.univ }) => 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} [Fintype α] [CommMonoid β] (f : { a : α // a ∈ Finset.univ } → β) : (Finset.prod (Finset.attach Finset.univ) fun (x : { x : α // x ∈ Finset.univ }) => 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} [DecidableEq α] [Fintype α] [AddCommMonoid β] {δ : α → Type u_4} {t : (a : α) → Finset (δ a)} (f : ((a : α) → a ∈ Finset.univ → δ a) → β) : (Finset.sum (Finset.pi Finset.univ t) fun (x : (a : α) → a ∈ Finset.univ → δ a) => f x) = Finset.sum (Fintype.piFinset t) fun (x : (a : α) → δ a) => f fun (a : α) (x_1 : a ∈ Finset.univ) => 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) and Fintype.piFinset t is a Finset (Π a, t a).

theorem Finset.prod_univ_pi {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [CommMonoid β] {δ : α → Type u_4} {t : (a : α) → Finset (δ a)} (f : ((a : α) → a ∈ Finset.univ → δ a) → β) : (Finset.prod (Finset.pi Finset.univ t) fun (x : (a : α) → a ∈ Finset.univ → δ a) => f x) = Finset.prod (Fintype.piFinset t) fun (x : (a : α) → δ a) => f fun (a : α) (x_1 : a ∈ Finset.univ) => 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) and Fintype.piFinset t is a Finset (Π a, t a).

theorem Finset.prod_univ_sum {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [CommSemiring β] {δ : α → Type u_1} [(a : α) → DecidableEq (δ a)] {t : (a : α) → Finset (δ a)} {f : (a : α) → δ a → β} : (Finset.prod Finset.univ fun (a : α) => Finset.sum (t a) fun (b : δ a) => f a b) = Finset.sum (Fintype.piFinset t) fun (p : (a : α) → δ a) => 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_4) [Fintype α] {R : Type u_5} [CommSemiring R] (a : R) (b : R) : (Finset.sum Finset.univ fun (s : Finset α) => a ^ Finset.card s * b ^ (Fintype.card α - Finset.card s)) = (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 Function.Bijective.sum_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] [AddCommMonoid γ] {f : α → β} (hf : Function.Bijective f) (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} [Fintype α] [Fintype β] [CommMonoid γ] {f : α → β} (hf : Function.Bijective f) (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} [Fintype α] [Fintype β] [AddCommMonoid γ] (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} [Fintype α] [Fintype β] [CommMonoid γ] (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} [Fintype α] [Fintype β] [AddCommMonoid γ] (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} [Fintype α] [Fintype β] [CommMonoid γ] (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} [AddCommMonoid α] (f : ℕ → α) (n : ℕ) : (Finset.sum Finset.univ fun (i : Fin n) => f ↑i) = Finset.sum (Finset.range n) 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} [CommMonoid α] (f : ℕ → α) (n : ℕ) : (Finset.prod Finset.univ fun (i : Fin n) => f ↑i) = Finset.prod (Finset.range n) 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_2} [AddCommMonoid β] {n : ℕ} (c : Fin n → β) : (Finset.sum Finset.univ fun (i : Fin n) => c i) = Finset.sum (Finset.range n) fun (i : ℕ) => if h : i < n then c { val := i, isLt := h } else 0

theorem Finset.prod_fin_eq_prod_range {β : Type u_2} [CommMonoid β] {n : ℕ} (c : Fin n → β) : (Finset.prod Finset.univ fun (i : Fin n) => c i) = Finset.prod (Finset.range n) fun (i : ℕ) => if h : i < n then c { val := i, isLt := 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) : (Finset.sum (Set.toFinset {x : α | p x}) fun (a : α) => f a) = Finset.sum Finset.univ fun (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) : (Finset.prod (Set.toFinset {x : α | p x}) fun (a : α) => f a) = Finset.prod Finset.univ fun (a : Subtype p) => f ↑a

theorem Finset.sum_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [Fintype β] [AddCommMonoid γ] (s : Finset α) (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_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [Fintype β] [CommMonoid γ] (s : Finset α) (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} [Fintype α] [DecidableEq β] [Fintype β] [AddCommMonoid γ] (f : α → β) (g : α → γ) : (Finset.sum Finset.univ fun (b : β) => Finset.sum Finset.univ fun (a : { a : α // f a = b }) => g ↑a) = Finset.sum Finset.univ fun (a : α) => g a

theorem Fintype.prod_fiberwise {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq β] [Fintype β] [CommMonoid γ] (f : α → β) (g : α → γ) : (Finset.prod Finset.univ fun (b : β) => Finset.prod Finset.univ fun (a : { a : α // f a = b }) => g ↑a) = Finset.prod Finset.univ fun (a : α) => g 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 → β) : (Finset.prod Finset.univ fun (a : α) => dite (p a) (f a) (g a)) = (Finset.prod Finset.univ fun (a : { a : α // p a }) => f ↑a (_ : p ↑a)) * Finset.prod Finset.univ fun (a : { a : α // ¬p a }) => g ↑a (_ : ¬p ↑a)

theorem Fintype.sum_sum_elim {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [Fintype α₁] [Fintype α₂] [AddCommMonoid M] (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_4} {α₂ : Type u_5} {M : Type u_6} [Fintype α₁] [Fintype α₂] [CommMonoid M] (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_4} {α₂ : Type u_5} {M : Type u_6} [Fintype α₁] [Fintype α₂] [AddCommMonoid M] (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_4} {α₂ : Type u_5} {M : Type u_6} [Fintype α₁] [Fintype α₂] [CommMonoid M] (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₂)

@[simp]

theorem Fintype.sum_prod_type {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [AddCommMonoid γ] {f : α₁ × α₂ → γ} : (Finset.sum Finset.univ fun (x : α₁ × α₂) => f x) = Finset.sum Finset.univ fun (x : α₁) => Finset.sum Finset.univ fun (y : α₂) => f (x, y)

@[simp]

theorem Fintype.prod_prod_type {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [CommMonoid γ] {f : α₁ × α₂ → γ} : (Finset.prod Finset.univ fun (x : α₁ × α₂) => f x) = Finset.prod Finset.univ fun (x : α₁) => Finset.prod Finset.univ fun (y : α₂) => f (x, y)

theorem Fintype.sum_prod_type' {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [AddCommMonoid γ] {f : α₁ → α₂ → γ} : (Finset.sum Finset.univ fun (x : α₁ × α₂) => f x.1 x.2) = Finset.sum Finset.univ fun (x : α₁) => Finset.sum Finset.univ fun (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 : α₁ → α₂ → γ} : (Finset.prod Finset.univ fun (x : α₁ × α₂) => f x.1 x.2) = Finset.prod Finset.univ fun (x : α₁) => Finset.prod Finset.univ fun (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 : α₁ × α₂ → γ} : (Finset.sum Finset.univ fun (x : α₁ × α₂) => f x) = Finset.sum Finset.univ fun (y : α₂) => Finset.sum Finset.univ fun (x : α₁) => f (x, y)

theorem Fintype.prod_prod_type_right {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [CommMonoid γ] {f : α₁ × α₂ → γ} : (Finset.prod Finset.univ fun (x : α₁ × α₂) => f x) = Finset.prod Finset.univ fun (y : α₂) => Finset.prod Finset.univ fun (x : α₁) => f (x, y)

theorem Fintype.sum_prod_type_right' {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [Fintype α₁] [Fintype α₂] [AddCommMonoid γ] {f : α₁ → α₂ → γ} : (Finset.sum Finset.univ fun (x : α₁ × α₂) => f x.1 x.2) = Finset.sum Finset.univ fun (y : α₂) => Finset.sum Finset.univ fun (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 : α₁ → α₂ → γ} : (Finset.prod Finset.univ fun (x : α₁ × α₂) => f x.1 x.2) = Finset.prod Finset.univ fun (y : α₂) => Finset.prod Finset.univ fun (x : α₁) => f x y

An uncurried version of Finset.prod_prod_type_right.