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.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 af 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 af 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 bf 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 bf 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 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} [CommMonoid M] {ι : Type u_5} [Subsingleton ι] {s : Finset ι} {f : ιM} {b : M} (h : (Finset.prod s fun (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.

@[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.pi s t).card = Finset.prod s fun (a : α) => (t a).card
@[simp]
theorem Fintype.card_piFinset {α : Type u_1} [DecidableEq α] [Fintype α] {δ : αType u_4} (t : (a : α) → Finset (δ a)) :
(Fintype.piFinset t).card = Finset.prod Finset.univ fun (a : α) => (t a).card
@[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 β] :
@[simp]
theorem card_vector {α : Type u_1} [Fintype α] (n : ) :
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 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 ) * Finset.prod Finset.univ fun (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) :
(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.