Fintype.sum_sum_type
theorem Fintype.sum_sum_type :
∀ {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [inst : Fintype α₁] [inst_1 : Fintype α₂]
[inst_2 : AddCommMonoid M] (f : α₁ ⊕ α₂ → M),
(Finset.univ.sum fun x => f x) =
(Finset.univ.sum fun a₁ => f (Sum.inl a₁)) + Finset.univ.sum fun a₂ => f (Sum.inr a₂)
The theorem `Fintype.sum_sum_type` states that for any two types `α₁` and `α₂`, and a type `M` with an instance of `AddCommMonoid`, and a function `f` from the sum type `α₁ ⊕ α₂` to `M`, the summation of `f` over all elements of the sum type `α₁ ⊕ α₂` is equal to the sum of `f` applied to all elements of `α₁` (with `Sum.inl`) plus the sum of `f` applied to all elements of `α₂` (with `Sum.inr`). Essentially, it asserts that summing over a disjoint union of types corresponds to summing over each type individually and then adding the two sums.
More concisely: For any type `α₁ ⊕ α₂`, function `f` from `α₁ ⊕ α₂` to an additive commutative monoid `M`, and elements `x₁ : α₁` and `x₂ : α₂`, `∑ i, f (i : α₁ ⊕ α₂) = ∑ x₁ : α₁, f (Sum.inl x₁) + ∑ x₂ : α₂, f (Sum.inr x₂)`.
|
Fintype.sum_eq_single
theorem Fintype.sum_eq_single :
∀ {α : Type u_1} {M : Type u_4} [inst : Fintype α] [inst_1 : AddCommMonoid M] {f : α → M} (a : α),
(∀ (x : α), x ≠ a → f x = 0) → (Finset.univ.sum fun x => f x) = f a
This theorem, `Fintype.sum_eq_single`, states that for any type `α` with a finite number of instances (as indicated by `Fintype α`) and any type `M` with addition and commutativity (as indicated by `AddCommMonoid M`), given a function `f` from `α` to `M` and an element `a` of `α`, if `f(x)` equals zero for all `x` in `α` that are not equal to `a`, then the sum of `f(x)` for all `x` in the universal finite set of `α` is equal to `f(a)`. In mathematical terms, this could be expressed as $\sum_{x \in X} f(x) = f(a)$ for $f(x) = 0$ when $x \neq a$, where the sum ranges over all elements in the finite set.
More concisely: For a finite type `α` and an `AddCommMonoid M` with function `f` from `α` to `M` such that `f(x) = 0` for all `x ≠ a`, the sum of `f(x)` over `α` equals `f(a)`.
|
Fintype.prod_sum_type
theorem Fintype.prod_sum_type :
∀ {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [inst : Fintype α₁] [inst_1 : Fintype α₂] [inst_2 : CommMonoid M]
(f : α₁ ⊕ α₂ → M),
(Finset.univ.prod fun x => f x) =
(Finset.univ.prod fun a₁ => f (Sum.inl a₁)) * Finset.univ.prod fun a₂ => f (Sum.inr a₂)
The theorem `Fintype.prod_sum_type` states that for any types `α₁` and `α₂` with finite instances and any commutative monoid `M`, given a function `f` from the sum type of `α₁` and `α₂` to `M`, the product of `f` applied to each element of the universal finite set (which includes all elements from `α₁` and `α₂`) is equal to the product of applying `f` to each element of `α₁` and `α₂` separately and then multiplying these two results together. In mathematical terms, for all `f: α₁ ⊕ α₂ → M`, we have `∏ x in univ, f(x) = (∏ a₁ in univ, f(a₁)) * (∏ a₂ in univ, f(a₂))` when `f` is applied to the left summand a₁ or the right summand a₂ respectively.
More concisely: For any commutative monoid M and finite types α₁ and α₂, the product of a function from α₁ ⊕ α₂ to M over the universal set is equal to the product of applying the function to each element of α₁ and α₂ separately and multiplying the results.
|
Fintype.card_piFinset
theorem Fintype.card_piFinset :
∀ {ι : Type u_4} {α : ι → Type u_6} [inst : DecidableEq ι] [inst_1 : Fintype ι] (s : (i : ι) → Finset (α i)),
(Fintype.piFinset s).card = Finset.univ.prod fun i => (s i).card
The theorem `Fintype.card_piFinset` states that for all types `α` with decidable equality and for which a finite set exists (`Fintype α`), and for a function `δ` mapping elements of `α` to another type, given a function `t` that maps every element of `α` to a finite set of `δ a`, the cardinality of the `piFinset` generated by `t` is equal to the product of the cardinalities of the individual finite sets `t a` for each element `a` in the universal finite set of `α`. In mathematical terms, this theorem is about the cardinality of the product of finite sets.
More concisely: For any type `α` with decidable equality and a finite number of elements, and for a function `t : α → Set`, the cardinality of the product `∏ x : α. t x` equals the product of the cardinalities of the sets `t x` for all `x` in `α`.
|
Fintype.sum_prod_type_right'
theorem Fintype.sum_prod_type_right' :
∀ {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [inst : Fintype α₁] [inst_1 : Fintype α₂]
[inst_2 : AddCommMonoid γ] {f : α₁ → α₂ → γ},
(Finset.univ.sum fun x => f x.1 x.2) = Finset.univ.sum fun y => Finset.univ.sum fun x => f x y
This theorem, named `Fintype.sum_prod_type_right'`, states that for all types `γ`, `α₁`, `α₂` and given instances of `Fintype α₁`, and `Fintype α₂`, as well an instance of `AddCommMonoid γ`, and a function `f` mapping `α₁` and `α₂` to `γ`, the sum over the universal (finite) set of the function `f` applied to each pair `(x.1, x.2)` is equal to the sum on the universal set of the sum over the universal set of the function `f` applied to `(x, y)`. Basically, it's a statement about how the order of summation doesn't affect the final sum in this context.
More concisely: For any types `γ`, `α₁`, `α₂` with `Fintype α₁` and `Fintype α₂`, and given an AddCommMonoid `γ` and a function `f : α₁ × α₂ → γ`, the sum of `∑ x : α₁, ∑ y : α₂, f x y` equals `∑ (x, y) : α₁ × α₂, f x y`.
|
Fin.prod_univ_eq_prod_range
theorem Fin.prod_univ_eq_prod_range :
∀ {α : Type u_1} [inst : CommMonoid α] (f : ℕ → α) (n : ℕ),
(Finset.univ.prod fun i => f ↑i) = (Finset.range n).prod fun i => f i
The theorem `Fin.prod_univ_eq_prod_range` states that for any commutative monoid `α` and any function `f` from natural numbers to `α`, the product of `f` over all elements of a finite set of natural numbers `Fin n` (represented by `Finset.univ.prod`) is equivalent to the product of `f` over all natural numbers less than `n` (represented by `Finset.range n.prod`). In other words, it is saying that we obtain the same result whether we compute the product of the function over all elements of a finite set of size `n` or over the set of all natural numbers less than `n`.
More concisely: For any commutative monoid `α` and function `f` from natural numbers to `α`, the product of `f` over a finite set of natural numbers of size `n` equals the product of `f` over the natural numbers less than `n`.
|
Fintype.card_pi
theorem Fintype.card_pi :
∀ {ι : Type u_4} {α : ι → Type u_6} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Fintype (α i)],
Fintype.card ((i : ι) → α i) = Finset.univ.prod fun i => Fintype.card (α i)
The theorem `Fintype.card_pi` states that for any type `α` with decidable equality and is a finite type, and a function `β : α → Type u_4` where each `β a` is also a finite type, the cardinality of the function type `(a : α) → β a` (i.e., the number of all possible functions from `α` to `β a` for every `a` in `α`) is equal to the product of the cardinalities of `β a` for all `a` in the universal finite set of type `α`. In other words, the number of all possible functions from `α` to `β a` is the product of the number of elements in each `β a` over all `a` in `α`.
More concisely: For a finite type `α` with decidable equality and a function `β : α → Type u_4` where each `β a` is finite, the number of functions from `α` to `β` is the product of the cardinalities of `β a` for all `a` in `α`.
|
Finset.card_pi
theorem Finset.card_pi :
∀ {ι : Type u_4} {α : ι → Type u_6} [inst : DecidableEq ι] (s : Finset ι) (t : (i : ι) → Finset (α i)),
(s.pi t).card = s.prod fun i => (t i).card
The theorem `Finset.card_pi` states that for any given finite set `s` of a type `α` with decidable equality, and any function `t` that maps each element `a` of `α` to a finite set of a type `δ a`, the cardinality of the set of all functions (defined on elements of `s` and taking values in `t a` for `a ∈ s`) is equal to the product of the cardinalities of the finite sets `t a` for each element `a` in `s`. In other words, if we have a finite set and a function mapping each element of this set to another finite set, the number of all possible functions we can define is just the product of the sizes of each of the latter sets. This is the notion of product in the context of cardinality of sets of functions.
More concisely: For any finite set \(s\) of type \(\alpha\) with decidable equality and a function \(t: \alpha \rightarrow \prod\_{a:\alpha} Finset\ delta\_a\), the cardinality of \(Func(s, t)\) equals the product of the cardinalities of \(t\ a\) for all \(a \in s\).
|
Fintype.sum_bool
theorem Fintype.sum_bool :
∀ {α : Type u_1} [inst : AddCommMonoid α] (f : Bool → α), (Finset.univ.sum fun b => f b) = f true + f false := by
sorry
This theorem, `Fintype.sum_bool`, states that for any type `α` equipped with an addition operation (forming a commutative monoid), and for any function `f` from the boolean type `Bool` to `α`, the sum of the function `f` over all elements in the universal finite set of `Bool`, which includes `true` and `false`, is equal to the sum of the function applied to `true` and the function applied to `false`. In other words, `f(true) + f(false)` gives us the total sum of `f` over the boolean set `Bool`.
More concisely: For any commutative monoid additivity-preserving function `f` from `Bool` to a type `α` equipped with addition, `f(true) + f(false)` equals the sum of `f` over the finite set `Bool`.
|
Fintype.sum_prod_type'
theorem Fintype.sum_prod_type' :
∀ {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [inst : Fintype α₁] [inst_1 : Fintype α₂]
[inst_2 : AddCommMonoid γ] {f : α₁ → α₂ → γ},
(Finset.univ.sum fun x => f x.1 x.2) = Finset.univ.sum fun x => Finset.univ.sum fun y => f x y
The theorem `Fintype.sum_prod_type'` states that for any types `α₁`, `α₂`, and `γ`, where `α₁` and `α₂` are finite types (i.e., they have a finite number of distinct values), and `γ` is a type with an additive commutative monoid structure. Given a function `f` that takes an element from `α₁` and `α₂` and returns an element of type `γ`, the sum of the function `f` applied to every pair in the Cartesian product of `α₁` and `α₂` is equal to the sum of the function `f` applied to each element of `α₁` and the sum of the function `f` applied to each element of `α₂`. Essentially, this theorem is a version of the distributive law for sums over finite sets.
More concisely: For any finite types `α₁` and `α₂` and additive commutative monoid `γ`, the function `f` from the Cartesian product of `α₁` and `α₂` to `γ` satisfies `∑ i, j (f (i, j)) = (∑ i x₁:α₁.elm i).map f + (∑ j x₂:α₂.elm j).map f`, where `∑` denotes summation.
|
Fintype.eq_of_subsingleton_of_prod_eq
theorem Fintype.eq_of_subsingleton_of_prod_eq :
∀ {M : Type u_4} [inst : CommMonoid M] {ι : Type u_5} [inst_1 : Subsingleton ι] {s : Finset ι} {f : ι → M} {b : M},
(s.prod fun i => f i) = b → ∀ i ∈ s, f i = b
This theorem states that for any type `M` that is a commutative monoid and any subsingleton type `ι`, if the product of a finite set `s` of type `ι`, where each element of `s` is mapped to an element of `M` by a function `f`, is equal to a certain value `b`, then each element `i` in the set `s` when mapped by the function `f` will also equal to `b`. In other words, if a product over a finite set of a certain type results in a value, each term in that product will also equal that value.
More concisely: If `M` is a commutative monoid, `ι` is a subsingleton type, `s` is a finite set of elements from `ι`, `b` is the product of `s` in `M`, and `f : ι → M` is a function, then for all `i ∈ s`, `f i = b`.
|
Fintype.card_fun
theorem Fintype.card_fun :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] [inst_2 : Fintype β],
Fintype.card (α → β) = Fintype.card β ^ Fintype.card α
The theorem `Fintype.card_fun` states that for any two types `α` and `β`, where `α` has decidable equality and both `α` and `β` are finite types (i.e., they have a finite number of elements), the number of functions from `α` to `β` is equal to the number of elements in `β` raised to the power of the number of elements in `α`. In mathematical terms, if `|α|` represents the number of elements in `α` and `|β|` represents the number of elements in `β`, then the number of functions from `α` to `β` is `|β|^|α|`.
This theorem essentially tells us about the cardinality of the set of all functions from `α` to `β` when `α` and `β` are finite and `α` has decidable equality.
More concisely: For finite types `α` with decidable equality and any type `β`, the number of functions from `α` to `β` equals the power of `|β|` raised to the power of `|α|`.
|
Fintype.card_sigma
theorem Fintype.card_sigma :
∀ {ι : Type u_4} {α : ι → Type u_6} [inst : Fintype ι] [inst_1 : (i : ι) → Fintype (α i)],
Fintype.card (Sigma α) = Finset.univ.sum fun i => Fintype.card (α i)
The theorem `Fintype.card_sigma` states that for any type `α` and a function `β : α → Type u_5`, given that `α` and `β a` for all `a : α` are finite types (`Fintype`), the total number of elements in the dependent pair type `(Sigma β)` is equal to the sum of the number of elements in each `β a`, as `a` ranges over the universal finite set of type `α`. In other words, it expresses the cardinality of a disjoint union of finite sets in terms of the sum of the cardinalities of each individual set.
More concisely: The theorem `Fintype.card_sigma` asserts that the cardinality of the dependent sum of a family of finite types indexed by a finite type equals the sum of the cardinalities of each individual type.
|
Fintype.sum_prod_type
theorem Fintype.sum_prod_type :
∀ {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [inst : Fintype α₁] [inst_1 : Fintype α₂]
[inst_2 : AddCommMonoid γ] {f : α₁ × α₂ → γ},
(Finset.univ.sum fun x => f x) = Finset.univ.sum fun x => Finset.univ.sum fun y => f (x, y)
The theorem `Fintype.sum_prod_type` states that for any types `α₁` and `α₂`, each having a finite number of distinct values (denoted by `Fintype α₁` and `Fintype α₂`), and for any type `γ` that has an addition operation obeying the commutative property (denoted by `AddCommMonoid γ`), given a function `f` that maps pairs `(α₁, α₂)` to `γ`, the sum of the function `f` values over all pairs in the universal finite set (denoted by `Finset.univ`) is equal to the sum of the function `f` values over all individual elements of `α₁` and `α₂` in the universal finite set. In essence, this theorem is expressing the distributive property of multiplication over addition set in the context of finite sums over finite types.
More concisely: For any type `γ` with commutative addition, and functions `f : (Fintype α₁ × Fintype α₂) → γ`, the sum of `f` over the universal finite set is equal to the sum of the function values over `α₁` and `α₂` separately.
|
Fintype.prod_prod_type_right'
theorem Fintype.prod_prod_type_right' :
∀ {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [inst : Fintype α₁] [inst_1 : Fintype α₂] [inst_2 : CommMonoid γ]
{f : α₁ → α₂ → γ},
(Finset.univ.prod fun x => f x.1 x.2) = Finset.univ.prod fun y => Finset.univ.prod fun x => f x y
This theorem, titled "Fintype.prod_prod_type_right'", states that for any given types `α₁` and `α₂`, which are finite types, and `γ` that is a commutative monoid, and for any function `f` from `α₁ × α₂` to `γ`, the product over the universal finset (`Finset.univ`) for the function `f` applied to each pair `(x.1, x.2)` is equal to the product over `Finset.univ` for the function `f` applied to each pair `(x, y)` where `(x, y)` is derived from the cross product of the universal finsets. This means that changing the order of the multiplication does not affect the final product, reflecting the commutative property of the monoid `γ`.
More concisely: For any commutative monoid γ and finite types α₁ and α₂, the product of a function from α₁ × α₂ to γ over the universal finsets of α₁ and α₂ is equal to the product of the function over their cross product finset.
|
Fintype.prod_prod_type'
theorem Fintype.prod_prod_type' :
∀ {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [inst : Fintype α₁] [inst_1 : Fintype α₂] [inst_2 : CommMonoid γ]
{f : α₁ → α₂ → γ},
(Finset.univ.prod fun x => f x.1 x.2) = Finset.univ.prod fun x => Finset.univ.prod fun y => f x y
This theorem states that for any types `α₁`, `α₂`, and `γ` where `α₁` and `α₂` are finite (i.e., there exists a finite list of all their elements) and `γ` is a commutative monoid (i.e., a set with an associative binary operation that has an identity element and each element has an inverse), and for any function `f` mapping pairs of elements from `α₁` and `α₂` to `γ`, the product over the universal finite set of `α₁ x α₂` (i.e., all pairs `(x.1, x.2)` where `x.1` is from `α₁` and `x.2` is from `α₂`) of `f` applied to each pair is equal to the product over the universal finite set of `α₁` of the product over the universal finite set of `α₂` of `f` applied to each element of `α₁` and `α₂`. In simpler terms, this theorem is a mathematical expression of the distributive law of multiplication over addition (though here the "addition" is instead a function application) applied to finite sets.
More concisely: For any finite types `α₁` and `α₂`, and any commutative monoid `γ`, the function `f` mapping pairs from `α₁ × α₂` to `γ` satisfies the distributive property: `∏ (x : α₁ × α₂) f x = ∏ x₁ : α₁ ∏ x₂ : α₂ f x₁ x₂`.
|
Fintype.eq_of_subsingleton_of_sum_eq
theorem Fintype.eq_of_subsingleton_of_sum_eq :
∀ {M : Type u_4} [inst : AddCommMonoid M] {ι : Type u_5} [inst_1 : Subsingleton ι] {s : Finset ι} {f : ι → M}
{b : M}, (s.sum fun i => f i) = b → ∀ i ∈ s, f i = b
This theorem states that if a sum of function values over a finite set of a subsingleton type equals a particular value, then each term in the sum must also equal that value. Here, `M` is a type with an addition operation that's both commutative and associative, `ι` is a subsingleton type (i.e., a type with at most one element), `s` is a finite set of elements of type `ι`, `f` is a function mapping elements of type `ι` to elements of type `M`, and `b` is an element of type `M`. The theorem asserts that if the sum of `f(i)` over all `i` in `s` equals `b`, then for every `i` in `s`, `f(i)` equals `b`.
More concisely: If the sum of the values of a function `f` over a finite set `s` of a subsingleton type `ι` equals a constant `b`, then each function value `f(i)` for `i` in `s` equals `b`.
|
Fin.sum_univ_eq_sum_range
theorem Fin.sum_univ_eq_sum_range :
∀ {α : Type u_1} [inst : AddCommMonoid α] (f : ℕ → α) (n : ℕ),
(Finset.univ.sum fun i => f ↑i) = (Finset.range n).sum fun i => f i
The theorem `Fin.sum_univ_eq_sum_range` states that for any natural number `n`, and for any function `f` from the natural numbers to a type `α` that is an additive commutative monoid, the sum of `f` over all elements in `fin n` (the finite set of natural numbers less than `n`) is equal to the sum of `f` over all elements in the set `finset.range n` (also the set of natural numbers less than `n`). Essentially, this theorem shows that these two ways of summing a function over a range of natural numbers are equivalent.
More concisely: For any additive commutative monoid type `α` and natural number `n`, the sum of a function from `Fin n` to `α` is equal to the sum of the restriction of that function to `finset.range n`.
|
Finset.sum_fin_eq_sum_range
theorem Finset.sum_fin_eq_sum_range :
∀ {β : Type u_2} [inst : AddCommMonoid β] {n : ℕ} (c : Fin n → β),
(Finset.univ.sum fun i => c i) = (Finset.range n).sum fun i => if h : i < n then c ⟨i, h⟩ else 0
This theorem, `Finset.sum_fin_eq_sum_range`, states that for any type `β` which is an additive commutative monoid and for any natural number `n`, if we have a function `c` which maps from a finite set of size `n` to `β`, then the sum of the function `c` over the entire universal finite set is equal to the sum of the function `c` over the range `n` with an additional condition: if a number `i` is less than `n`, then we consider `c` at `i`, otherwise we consider `0`. In other words, the sum of a function over a finite set is same as the sum of the function over all natural numbers less than the size of the set, where the function is zero for numbers not in the set.
More concisely: For any additive commutative monoid type `β` and natural number `n`, the sum of a function from a finite set of size `n` to `β` equals the sum of applying the function to the first `n` natural numbers and zero for the remaining ones.
|