Fin.sum_univ_zero
theorem Fin.sum_univ_zero :
∀ {β : Type u_2} [inst : AddCommMonoid β] (f : Fin 0 → β), (Finset.univ.sum fun i => f i) = 0
The theorem `Fin.sum_univ_zero` states that for any type `β` that has an additive commutative monoid structure, the sum over a set of type `Fin 0` (which is empty), under any function `f: Fin 0 → β`, is equal to zero. This is because summing over an empty set, regardless of the function, always results in the additive identity, which is zero in this case.
More concisely: For any additive commutative monoid `β`, the sum of elements from the empty set to `β`, under any function, equals the additive identity `0` in `β`.
|
Fin.prod_univ_zero
theorem Fin.prod_univ_zero :
∀ {β : Type u_2} [inst : CommMonoid β] (f : Fin 0 → β), (Finset.univ.prod fun i => f i) = 1
The theorem `Fin.prod_univ_zero` states that for any type `β` equipped with a commutative monoid structure, and any function `f` from the set `Fin 0` (which is the finite type with zero elements, i.e., an empty set) to `β`, the product over all elements in the universal set (`Finset.univ`, which is also empty in this case) of the values of `f` is equal to `1` (the identity for multiplication in the commutative monoid `β`). This is essentially due to the fact that the product over an empty set is defined to be the multiplicative identity, which is `1` in this context.
More concisely: For any commutative monoid `β` and empty function `f` from the finite type with zero elements to `β`, the product of the values of `f` is equal to the monoid identity `1`.
|
Fin.sum_univ_succAbove
theorem Fin.sum_univ_succAbove :
∀ {β : Type u_2} [inst : AddCommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) (x : Fin (n + 1)),
(Finset.univ.sum fun i => f i) = f x + Finset.univ.sum fun i => f (x.succAbove i)
This theorem states that for any type `β` that forms an additive commutative monoid, any natural number `n`, and any function `f` from `Fin (n + 1)` to `β`, the sum of `f` over all elements of `Fin (n + 1)` equals the sum of `f x` for some `x` in `Fin (n + 1)` and the sum of `f` over all elements of `x.succAbove i`, where `i` ranges over all elements of the universal `Finset`. The `x.succAbove i` operation describes the remaining elements in `Fin (n + 1)` after `x`. The result holds for all `x` in `Fin (n + 1)`.
More concisely: For any additive commutative monoid type `β` and function `f` from `Fin (n + 1)` to `β`, the sum of `f` over all elements of `Fin (n + 1)` equals the sum of `f x` for some `x` in `Fin (n + 1)` and the sum of `f` over the remaining elements after `x`.
|
Fin.sum_univ_castSucc
theorem Fin.sum_univ_castSucc :
∀ {β : Type u_2} [inst : AddCommMonoid β] {n : ℕ} (f : Fin (n + 1) → β),
(Finset.univ.sum fun i => f i) = (Finset.univ.sum fun i => f i.castSucc) + f (Fin.last n)
The theorem `Fin.sum_univ_castSucc` states that for any type `β` that forms an additive commutative monoid, and for any function `f` from `Fin (n + 1)` to `β`, the total sum of `f` evaluated at each element in the universal set of `Fin (n + 1)` equals the sum of `f` evaluated at the element obtained by embedding each element in the universal set of `Fin (n + 1)` into `Fin (n + 2)`, plus `f` evaluated at the maximum element in `Fin (n + 1)`. In mathematical terms, this theorem asserts that $\sum_{i=0}^{n+1} f(i) = \left(\sum_{i=0}^{n} f(i+1)\right) + f(n+1)$, where $f$ is a function defined on a finite index set.
More concisely: For any additive commutative monoid type `β` and function `f` from `Fin (n + 1)` to `β`, the sum of `f` over the universal set of `Fin (n + 1)` equals the sum over `Fin (n)` of `f`'s values at the successor indices, plus `f`'s value at the maximum index.
|
Fin.prod_univ_succAbove
theorem Fin.prod_univ_succAbove :
∀ {β : Type u_2} [inst : CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) (x : Fin (n + 1)),
(Finset.univ.prod fun i => f i) = f x * Finset.univ.prod fun i => f (x.succAbove i)
The theorem `Fin.prod_univ_succAbove` states that for any finite commutative monoid `β`, any natural number `n`, and any function `f` from `Fin (n + 1)` to `β`, and any `x` in `Fin (n + 1)`, the product of `f` over all elements in `Fin (n + 1)` is equal to the product of `f x` times the product of `f` over the elements in `Fin (n + 1)`, where the latter product excludes `x` by using the `Fin.succAbove` function.
In simpler terms, it states that the total product of a function over a finite set is equal to the product of the function's value at a certain point and the product of the function's value at the rest of the points in the set.
More concisely: For any finite commutative monoid β, natural number n, and function f from Fin (n + 1) to β, the product of f over Fin (n + 1) equals the product of f (x) and the product of f over Fin (n + 1) \{x}, where x is an element of Fin (n + 1) and Fin.succAbove is used to exclude it.
|
Fin.sum_univ_succ
theorem Fin.sum_univ_succ :
∀ {β : Type u_2} [inst : AddCommMonoid β] {n : ℕ} (f : Fin (n + 1) → β),
(Finset.univ.sum fun i => f i) = f 0 + Finset.univ.sum fun i => f i.succ
The theorem `Fin.sum_univ_succ` states that for any natural number `n`, and any function `f` mapping from the finite set `Fin (n + 1)` to a type `β` equipped with an additive commutative monoid structure, the sum of the function `f` over all elements of `Fin (n + 1)` equals the sum of `f 0` and the sum of `f` applied to the "successor" of the remaining elements in the set. Here, the "successor" of an element is obtained via the function `Fin.succ`.
More concisely: For any natural number `n` and additive commutative monoid-valued function `f` on `Fin (n + 1)`, the sum of `f` over all elements equals the sum of `f 0` and the sum of `f` over the remaining elements, where the remaining elements are those indexed by `Fin.succ`.
|
List.sum_ofFn
theorem List.sum_ofFn :
∀ {α : Type u_1} [inst : AddCommMonoid α] {n : ℕ} {f : Fin n → α},
(List.ofFn f).sum = Finset.univ.sum fun i => f i
This theorem states that for any given type `α` that has an additive commutative monoid structure, any natural number `n`, and any function `f` from the finite set `Fin n` to `α`, the sum of the list created by applying `f` to each element in `Fin n` (i.e., `List.sum (List.ofFn f)`) is equal to the sum of `f` applied to each element in the universal finite set (i.e., `Finset.sum Finset.univ fun i => f i`). In simpler terms, it states that the sum of the elements of a list created by applying a function to each element of a finite set is equivalent to the sum of the function's values over the entire finite set.
More concisely: For any additive commutative monoid type `α`, function `f` from a finite set `Fin n` to `α`, and natural number `n`, the sum of the list `[f i | i ∈ Fin n]` equals the sum of `f` over the universal finite set `Finset.univ`.
|
Fin.prod_const
theorem Fin.prod_const :
∀ {α : Type u_1} [inst : CommMonoid α] (n : ℕ) (x : α), (Finset.univ.prod fun _i => x) = x ^ n
This theorem, named `Fin.prod_const`, states that for any types `α` (which has a `CommMonoid` instance) and a natural number `n`, and an element `x` of type `α`, the product of `x` for each element in the universal finite set `Finset.univ` (which iterates over all elements of `α`), is equal to `x` raised to the power `n`. It essentially says that the product of a constant value over a finite set is equal to the constant raised to the power of the size of the set.
More concisely: For any type `α` with a `CommMonoid` instance, and any natural number `n` and element `x` of `α`, the product of `x` over all elements in the universal finite set `Finset.univ` equals `x` raised to the power `n`.
|
Fin.neg_partialSum_add_eq_contractNth
theorem Fin.neg_partialSum_add_eq_contractNth :
∀ {n : ℕ} {G : Type u_3} [inst : AddGroup G] (g : Fin (n + 1) → G) (j : Fin (n + 1)) (k : Fin n),
-Fin.partialSum g (j.succ.succAbove k.castSucc) + Fin.partialSum g (j.succAbove k).succ =
j.contractNth (fun x x_1 => x + x_1) g k
This theorem named `Fin.neg_partialSum_add_eq_contractNth` is about certain properties of partial sums over a tuple (sequence) of elements from an additive group `G`. Given a tuple `(g₀, g₁, ..., gₙ)` in `Gⁿ⁺¹`, the theorem describes three different behaviors depending on the relative values of `k` and `j`.
1. If `k < j`, the theorem states that the negation of the sum of the first `k` elements plus the sum of the first `k+1` elements equals the `(k+1)`th element, i.e., `- (g₀ + g₁ + ... + gₖ₋₁) + (g₀ + g₁ + ... + gₖ) = gₖ`.
2. If `k = j`, the theorem articulates that the negation of the sum of the first `k` elements plus the sum of the first `k+2` elements equals the sum of the `(k+1)`th and `(k+2)`th elements, i.e., `- (g₀ + g₁ + ... + gₖ₋₁) + (g₀ + g₁ + ... + gₖ₊₁) = gₖ + gₖ₊₁`.
3. If `k > j`, the theorem asserts that the negation of the sum of the first `k+1` elements plus the sum of the first `k+2` elements equals the `(k+2)`th element, i.e., `- (g₀ + g₁ + ... + gₖ) + (g₀ + g₁ + ... + gₖ₊₁) = gₖ₊₁`.
This theorem is useful for defining group cohomology.
More concisely: For any tuple `(g₀, g₁, ..., gₙ)` in an additive group `G`, the negation of the sum of the first `k` elements plus the sum of the first `k+1` elements equals the `(k+1)`th element when `k < j`, the sum of the `(k+1)`th and `(k+2)`th elements when `k = j`, and the `(k+2)`th element when `k > j`.
|
Fin.sum_univ_two
theorem Fin.sum_univ_two :
∀ {β : Type u_2} [inst : AddCommMonoid β] (f : Fin 2 → β), (Finset.univ.sum fun i => f i) = f 0 + f 1
The theorem `Fin.sum_univ_two` states that for any function `f` from a two-element finite type (`Fin 2`) to a type `β` that forms an additive commutative monoid, computing the sum of `f` over all elements of the universal set (`Finset.univ`) results in the sum of `f` evaluated at `0` and `f` evaluated at `1`. In other words, if we apply `f` to each element of a two-element set and sum the results, we get `f(0) + f(1)`.
More concisely: For any additive commutative monoid β and function f from a two-element finite set to β, the sum of f over the universal set is equal to f(0) + f(1).
|
Finset.sum_range
theorem Finset.sum_range :
∀ {β : Type u_2} [inst : AddCommMonoid β] {n : ℕ} (f : ℕ → β),
((Finset.range n).sum fun i => f i) = Finset.univ.sum fun i => f ↑i
This theorem, named `Finset.sum_range`, states that for any given type `β` that is an additive commutative monoid, any natural number `n`, and any function `f` from natural numbers to `β`, the sum of the function `f` over the range of natural numbers less than `n` is equal to the sum of the function `f` over all elements in the universal finite set of natural numbers. Concretely, if we apply the function `f` to each natural number less than `n` and take the sum, it will be the same as if we applied `f` to every natural number in the finite universal set and summed the results.
More concisely: For any additive commutative monoid type `β`, natural number `n`, and function `f` from natural numbers to `β`, the sum of `f` over the finite set of natural numbers less than `n` equals the sum of `f` over the universal set of natural numbers.
|
Fin.prod_univ_succ
theorem Fin.prod_univ_succ :
∀ {β : Type u_2} [inst : CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β),
(Finset.univ.prod fun i => f i) = f 0 * Finset.univ.prod fun i => f i.succ
The theorem `Fin.prod_univ_succ` states that for any commutative monoid `β`, natural number `n`, and function `f` from the finite set `Fin (n + 1)` to `β`, the product of `f` applied to every element in the universal finite set (which includes all elements of `Fin (n + 1)`) is equal to the product of `f 0` and the product of `f` applied to every successor element in the universal finite set. In simpler terms, it decomposes the product over a finite set into the product of the first element and the product of the remaining elements.
More concisely: For any commutative monoid β, natural number n, and function f from Fin (n + 1) to β, the product of f evaluated at the universal finite set equals the product of f evaluated at 0 and the product of f evaluated at the successor elements in the universal finite set.
|
Fin.prod_univ_castSucc
theorem Fin.prod_univ_castSucc :
∀ {β : Type u_2} [inst : CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β),
(Finset.univ.prod fun i => f i) = (Finset.univ.prod fun i => f i.castSucc) * f (Fin.last n)
The theorem `Fin.prod_univ_castSucc` states that for any function `f` from the finite set `Fin (n + 1)` to a type `β` that forms a commutative monoid, the product of `f` over all elements of `Fin (n + 1)` is equal to the product of `f` over all elements in the form `Fin.castSucc i` multiplied by `f` evaluated at the last element of `Fin (n + 1)`. Here, `Fin (n + 1)` represents the finite set of natural numbers less than `n + 1`, `Fin.castSucc` is a function that embeds a number in `Fin n` into `Fin (n + 1)`, and `Fin.last n` stands for the greatest value in `Fin (n + 1)`. Essentially, it verifies the product of the function values over the entire set can be partitioned into the product over the embedded lower index set and the function value at the last element.
More concisely: For any commutative monoid-valued function `f` on `Fin (n + 1)`, the product of `f` over all elements equals the product over `Fin.castSucc` elements multiplied by `f` evaluated at `Fin.last (n + 1)`.
|
Fin.inv_partialProd_mul_eq_contractNth
theorem Fin.inv_partialProd_mul_eq_contractNth :
∀ {n : ℕ} {G : Type u_3} [inst : Group G] (g : Fin (n + 1) → G) (j : Fin (n + 1)) (k : Fin n),
(Fin.partialProd g (j.succ.succAbove k.castSucc))⁻¹ * Fin.partialProd g (j.succAbove k).succ =
j.contractNth (fun x x_1 => x * x_1) g k
This theorem makes a statement about a sequence of elements from a group G. We have a tuple (g₀, g₁, ..., gₙ) of elements of G, indexed by natural numbers. The theorem specifies three conditions based on the relationship between integers k and j.
1. If k is less than j, it states that the inverse of the product of the first k elements (starting from g₀ to gₖ₋₁) multiplied by the product of the first k+1 elements (from g₀ to gₖ) equals gₖ.
2. If k equals j, it asserts that the inverse of the product of the first k elements (from g₀ to gₖ₋₁) multiplied by the product of the first k+2 elements (from g₀ to gₖ₊₁) equals the product of gₖ and gₖ₊₁.
3. If k is greater than j, it claims that the inverse of the product of the first k+1 elements (from g₀ to gₖ) multiplied by the product of the first k+2 elements (from g₀ to gₖ₊₁) equals gₖ₊₁.
This theorem is useful for defining group cohomology.
More concisely: For all natural numbers k and j with k ≤ j, if (g\_0, g\_1, ..., g\_n) is a sequence in a group G, then the following equality holds:
- If k < j, then gₖ = (∏_{i=0}^{k-1} g\_i)⁻¹ ∏_{i=0}^{k} g\_i
- If k = j, then gₖ \* gₖ₊₁ = (∏_{i=0}^{k-1} g\_i)⁻¹ ∏_{i=0}^{k+1} g\_i
- If k > j, then gₖ₊₁ = (∏_{i=0}^{k} g\_i)⁻¹ ∏_{i=0}^{k+1} g\_i.
This theorem relates the products and inverses of subsequences of a group element sequence.
|
Fin.sum_univ_one
theorem Fin.sum_univ_one :
∀ {β : Type u_2} [inst : AddCommMonoid β] (f : Fin 1 → β), (Finset.univ.sum fun i => f i) = f 0
The theorem `Fin.sum_univ_one` states that for any commutative, associative addition operation on a type `β` (denoted `AddCommMonoid β`), and any function `f` from a singleton set (a set with one element, denoted `Fin 1`) to `β`, the sum of the function `f` over the universal set (which includes every element of the domain of the function) is equal to the value of the function at 0. This essentially means that for a function defined on a singleton set, the sum of the function's values across all elements in the set (which in this case is just one element, 0) is just the function's value at 0.
More concisely: For any commutative, associative addition operation on a type `β` and any function `f` from a singleton set to `β`, the sum of `f` over the universal set equals the value of `f` at 0. (Or, more mathematically: For every `AddCommMonoid β` and every `f : Fin 1 → β`, `∑ i in Fin 1, f i = f 0`.)
|
Fin.prod_univ_two
theorem Fin.prod_univ_two :
∀ {β : Type u_2} [inst : CommMonoid β] (f : Fin 2 → β), (Finset.univ.prod fun i => f i) = f 0 * f 1
The theorem `Fin.prod_univ_two` states that for any type `β` where `β` is a commutative monoid, and any function `f` from the 2-element finite type to `β`, the product of `f x` as `x` ranges over all elements of the universal finite set is equal to the product of `f` at 0 and `f` at 1. In other words, if we have a function `f` that takes a 2-element set to some commutative monoid, the product of `f` for all elements in the set equals to `f(0) * f(1)`.
More concisely: For any commutative monoid `β` and function `f` from the 2-element finite set to `β`, the product of `f x` over all `x` in the set equals `f 0 * f 1`.
|