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.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 : ι)
:
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 : ι)
:
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 β]
:
Fintype.card (α → β) = Fintype.card β ^ Fintype.card α
@[simp]
theorem
card_vector
{α : Type u_1}
[Fintype α]
(n : ℕ)
:
Fintype.card (Vector α n) = Fintype.card α ^ 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 (_ : 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.