List.headI_le_sum
theorem List.headI_le_sum : ∀ (L : List ℕ), L.headI ≤ L.sum
This theorem, `List.headI_le_sum`, states that for any list of natural numbers (`List ℕ`), the head element (`L.headI`) is always less than or equal to the sum of all elements in the list (`L.sum`). This theorem assumes that the default value for natural numbers is 0.
More concisely: For any list of natural numbers, the head element is less than or equal to the sum of all elements.
|
List.sum_eq_zero
theorem List.sum_eq_zero : ∀ {M : Type u_5} [inst : AddMonoid M] {l : List M}, (∀ x ∈ l, x = 0) → l.sum = 0
This theorem states that for any list `l` of elements of type `M`, where `M` is a type that forms an additive monoid, if every element `x` in the list `l` is equal to zero, then the sum of all elements in the list `l` is also zero. In other words, the sum of a list of zeros (in an additive monoid) is zero.
More concisely: If `l` is a list of elements from an additive monoid `M`, then the sum of `l` is zero if and only if every element in `l` is zero.
|
List.prod_set'
theorem List.prod_set' :
∀ {G : Type u_9} [inst : CommGroup G] (L : List G) (n : ℕ) (a : G),
(L.set n a).prod = L.prod * if hn : n < L.length then (L.get ⟨n, hn⟩)⁻¹ * a else 1
This theorem, `List.prod_set'`, states that for any list `L` of elements from a type `G` that forms a commutative group, any natural number `n`, and any group element `a`, the product of the elements in a list resulting from setting the `n`th element of `L` to `a` is equal to the product of the elements of `L` times the inverse of the `n`th element of `L` times `a`, if `n` is less than the length of `L`; otherwise, it is simply the product of the elements in `L`. This theorem provides an alternative version of `List.prod_set` specific to lists over a group.
More concisely: For any commutative group `G`, list `L` of length `n` from `G`, and natural number `i` (`0 ≤ i < n`), the product of the elements in `L` with the `i`th element replaced by `a` equals the product of the elements in `L` multiplied by the inverse of the `i`th element in `L` multiplied by `a`.
|
List.get?_zero_mul_tail_prod
theorem List.get?_zero_mul_tail_prod :
∀ {M : Type u_5} [inst : Monoid M] (l : List M), (l.get? 0).getD 1 * l.tail.prod = l.prod
This theorem states that, for any list `l` of elements of a given type `M` that forms a monoid, the product of the first element of the list (or 1 if the list is empty) and the product of the remaining elements of the list is equal to the product of all elements in the list. It's written in this way because the function `L.headI` that might be used to get the first element of the list returns an arbitrary value when the list is empty, so instead we use `(l.get? 0).getD 1`, which safely returns the first element or 1 if the list is empty.
More concisely: For any monoid `M` and list `l` of `M` elements, the product of the first element of `l` (or 1 if `l` is empty) and the product of the remaining elements equals the product of all elements in `l`.
|
List.sum_hom
theorem List.sum_hom :
∀ {M : Type u_5} {N : Type u_6} [inst : AddMonoid M] [inst_1 : AddMonoid N] (l : List M) {F : Type u_11}
[inst_2 : FunLike F M N] [inst_3 : AddMonoidHomClass F M N] (f : F), (List.map (⇑f) l).sum = f l.sum
The theorem `List.sum_hom` states that for any types `M` and `N` that form addition monoids, any list `l` of elements of type `M`, any type `F` that has an injective function-like behavior from `M` to `N` and respects the structure of an additive monoid homomorphism, and any function `f` of type `F`, the sum of the list obtained by mapping `f` over `l` is equal to the result of applying `f` to the sum of `l`. This reflects the distributivity of the sum over the function application.
More concisely: For any additive monoids M and N, any injective, additive monoid homomorphism F from M to N, and any list l of elements from M, the sum of the images of l under F is equal to the image of the sum of l under F.
|
List.sum_neg
theorem List.sum_neg : ∀ {G : Type u_9} [inst : AddCommGroup G] (L : List G), -L.sum = (List.map (fun x => -x) L).sum
This theorem, called `List.sum_neg`, states that for any given list `L` of elements from an additive commutative group `G`, the additive inverse of the sum of the elements in `L` equals to the sum of the additive inverses of each element in `L`. In other words, it's a list version of the `add_neg` property, which in mathematical notation can be written as: `-ΣL = Σ(-x)` for each `x` in `L`. This theorem establishes the distributivity of the negation operation over the summation operation in the context of lists containing elements from an additive commutative group.
More concisely: For any list `L` of elements from an additive commutative group `G`, the additive inverse of the sum of the list equals the sum of the additive inverses of its elements: `-Σx ∈ L x = Σx ∈ L (-x)`.
|
List.tail_sum
theorem List.tail_sum : ∀ (L : List ℕ), L.tail.sum = L.sum - L.headI
This theorem, `List.tail_sum`, states that for any list of natural numbers `L`, the sum of the elements in the tail of `L` is equal to the sum of all elements in `L` minus the head of `L`. This theorem assumes a default value of 0 for natural numbers, which suggests that if `L` is an empty list, its head is taken as 0.
More concisely: The sum of the elements in a list's tail is equal to the sum of all elements in the list minus its head.
|
List.length_pos_of_sum_ne_zero
theorem List.length_pos_of_sum_ne_zero : ∀ {M : Type u_5} [inst : AddMonoid M] (L : List M), L.sum ≠ 0 → 0 < L.length
This theorem states that for any type `M` that forms an additive monoid, if a list `L` of type `M` has a non-zero sum, then the length of the list must be greater than zero. In other words, any list whose elements add up to a non-zero value must have at least one element in it.
More concisely: If `M` is an additive monoid and `L : list M` has non-zero sum, then `#L > 0`. (Here, `#` denotes the length of a list.)
|
List.length_pos_of_sum_neg
theorem List.length_pos_of_sum_neg :
∀ {M : Type u_5} [inst : AddMonoid M] [inst_1 : Preorder M] (L : List M), L.sum < 0 → 0 < L.length
This theorem states that for any type `M` that is an additive monoid and has a preorder relation, any list `L` of type `M` that has a sum less than zero must have a positive length. In other words, if the sum of all the elements in the list is negative, then the list cannot be empty.
More concisely: If `M` is an additive monoid with a preorder relation, then any list `L` of type `M` with negative sum has positive length.
|
List.prod_cons
theorem List.prod_cons : ∀ {M : Type u_5} [inst : Monoid M] {l : List M} {a : M}, (a :: l).prod = a * l.prod
The theorem `List.prod_cons` states that for any type `M` that forms a monoid, any list `l` of elements of type `M`, and any element `a` of type `M`, the product of the list that results from prepending `a` to `l` is equal to `a` multiplied by the product of `l`. In other words, if you add an element to the start of a list and then calculate the product of the list, it's the same as if you multiplied that element with the product of the original list.
More concisely: For any monoid `M`, any list `l` of `M`, and any `a` in `M`, we have `a * List.foldl (fun _ x => x) l = List.foldl (fun x _ => x * a) l a`.
|
List.sum_set'
theorem List.sum_set' :
∀ {G : Type u_9} [inst : AddCommGroup G] (L : List G) (n : ℕ) (a : G),
(L.set n a).sum = L.sum + if hn : n < L.length then -L.get ⟨n, hn⟩ + a else 0
This theorem, `List.sum_set'`, provides an alternative version of `List.sum_set` for the case when the list is over a group. It states that, for any type `G` that forms an additive commutative group, any list `L` of elements of `G`, any natural number `n`, and any group element `a`, the sum of all elements in the list where the element at index `n` is replaced by `a` is equal to the original sum of the list plus, if `n` is less than the length of the list, `a` minus the original element at index `n`, otherwise 0.
More concisely: For any additive commutative group `G`, list `L` of `G`, natural number `n`, and group element `a`, the sum of the first `n-1` elements in `L`, the group element `a`, and the sum of the remaining elements in `L` is equal to the original sum of `L` plus `a` if `n` is less than the list length, otherwise equal to the original sum of `L`.
|
List.length_pos_of_prod_ne_one
theorem List.length_pos_of_prod_ne_one : ∀ {M : Type u_5} [inst : Monoid M] (L : List M), L.prod ≠ 1 → 0 < L.length
This theorem states that for any list of elements 'L' from a type 'M' which has a Monoid structure, if the product of all the elements in the list is not equal to the identity element (1), then the length of the list must be greater than zero. In other words, a list with a product that does not equal the identity must be a non-empty list.
More concisely: If `M` is a type with a monoid structure and `L` is a non-empty list of elements from `M` such that the product of `L` is not the identity element, then `#L ≠ 1`. (Here, `#L` denotes the product of all elements in the list `L`.)
|
List.sum_map_count_dedup_filter_eq_countP
theorem List.sum_map_count_dedup_filter_eq_countP :
∀ {α : Type u_2} [inst : DecidableEq α] (p : α → Bool) (l : List α),
(List.map (fun x => List.count x l) (List.filter p l.dedup)).sum = List.countP p l
This theorem asserts that for any type `α` with decidable equality and for any predicate `p` of type `α → Bool` and list `l` of type `α`, the sum of the counts of each element `x` in the list obtained by filtering `l` (after removing duplication) by `p` (i.e., keeping only those elements for which `p` returns true) is equal to the count of elements in `l` that satisfy `p`. In other words, it states that summing up the occurrences of each element in the filtered and deduplicated list is the same as counting the number of elements in the original list that satisfy the predicate `p`.
More concisely: For any type `α` with decidable equality, predicate `p` of type `α → Bool`, and list `l` of type `α`, the sum of the cardinalities of `p`-filtered and deduplicated sublists of `l` equals the cardinality of the subset of `l` satisfying `p`.
|
List.prod_singleton
theorem List.prod_singleton : ∀ {M : Type u_5} [inst : MulOneClass M] {a : M}, [a].prod = a
This theorem states that the product of a list containing a single element `a` is equal to `a` itself. Here, `M` is any type endowed with a multiplication operation and a special element called "one" (represented by the `MulOneClass` typeclass in Lean 4). The function `List.prod` computes the product of all elements in a list, starting from "one" and then multiplying each element in the list in order.
More concisely: For any type `M` with multiplication and a multiplicative identity `one`, the product of a list containing a single element `a` of type `M` is equal to `a`.
|
List.sum_cons
theorem List.sum_cons : ∀ {M : Type u_5} [inst : AddMonoid M] {l : List M} {a : M}, (a :: l).sum = a + l.sum
This theorem states that for any type `M` that is equipped with an additive monoid structure, any list of elements `l` of type `M`, and any element `a` of type `M`, the sum of the list obtained by prepending `a` to `l` is equal to `a` plus the sum of the list `l`. In other words, for a given list and an element, the sum of the new list starting with this element is the same as adding the element to the sum of the original list. This is analogous to the mathematical property of summation that the sum of a list with an additional term at the start is the additional term plus the sum of the original list.
More concisely: For any additive monoid `M`, any list `l` of elements in `M`, and any element `a` in `M`, the sum of the list `[a] ++ l` equals `a + sum l`, where `++` denotes list concatenation.
|
List.prod_eq_one
theorem List.prod_eq_one : ∀ {M : Type u_5} [inst : Monoid M] {l : List M}, (∀ x ∈ l, x = 1) → l.prod = 1
This theorem, `List.prod_eq_one`, states that for any type `M` that forms a `Monoid`, and for any list `l` of elements of type `M`, if every element `x` in the list `l` is equal to the multiplicative identity `1`, then the product of all elements in the list `l` (computed using the `List.prod` function defined above) is also equal to the multiplicative identity `1`. In other words, if every element of a list is the identity element of a monoid, then the product of all elements in the list is also the identity element.
More concisely: For any monoid `M` and list `l` of elements from `M` where every element is the identity `1`, the product of all elements in `l` is equal to the identity `1`.
|
List.sum_replicate
theorem List.sum_replicate : ∀ {M : Type u_5} [inst : AddMonoid M] (n : ℕ) (a : M), (List.replicate n a).sum = n • a
The theorem `List.sum_replicate` asserts that for any type `M` that forms an Additive Monoid, any natural number `n`, and any element `a` of type `M`, the sum of a list that is created by replicating `a` `n` times (i.e., `List.replicate n a`) is equal to `n` times `a` (denoted by `n • a` in Lean notation). In other words, it states that summing `n` copies of an element `a` in an additive monoid is the same as scaling `a` by `n`.
More concisely: For any additive monoid type `M`, natural number `n`, and element `a` in `M`, the sum of replicating `a` in a list of length `n` equals `n` times `a`.
|
List.drop_take_succ_join_eq_get
theorem List.drop_take_succ_join_eq_get :
∀ {α : Type u_2} (L : List (List α)) (i : Fin L.length),
List.drop (List.take (↑i) (List.map List.length L)).sum
(List.take (List.take (↑i + 1) (List.map List.length L)).sum L.join) =
L.get i
This theorem states that for a given list of lists `L` and an index `i`, if we join the sublists of `L` and then take a slice between two indices `A` and `B - 1`, where `A` is the sum of the lengths of sublists of `L` having indices less than `i`, and `B` is the sum of the lengths of sublists with indices less than or equal to `i`, we will get back the original sublist at index `i` of `L`. In other words, it explains a method to extract a specific sublist from a joined list of lists using the cumulative lengths of the sublists as slicing indices.
More concisely: For any list of lists `L` and index `i`, the sublist of the joined list `L.foldl (· ++) []` from index `sum (List.take i L) length` to `sum (List.take (Pred i) L) length` is equal to the original sublist at index `i` in `L`.
|
List.prod_hom
theorem List.prod_hom :
∀ {M : Type u_5} {N : Type u_6} [inst : Monoid M] [inst_1 : Monoid N] (l : List M) {F : Type u_11}
[inst_2 : FunLike F M N] [inst_3 : MonoidHomClass F M N] (f : F), (List.map (⇑f) l).prod = f l.prod
The theorem `List.prod_hom` states that for any two types `M` and `N` that are monoids, a list `l` of elements of type `M`, an object `F` that is a function-like structure from `M` to `N` and also a monoid homomorphism, and a function `f` of this structure, the product of the list obtained by mapping `f` over `l` is equal to the result of applying `f` to the product of `l`. In other words, given a monoid homomorphism from `M` to `N`, the action of the monoid homomorphism on the product of a list is the same as the product of the list obtained by acting the monoid homomorphism on each element of the list. This is a formalization of the homomorphism property $f(\prod l) = \prod (f(l))$ in the context of lists and monoids.
More concisely: Given a monoid homomorphism from type `M` to type `N`, the product of the image of a list `l` of elements from `M` under this homomorphism is equal to the image of the product of `l` under the same homomorphism. In other words, `f (prod l) = prod (map f l)` for a monoid homomorphism `f` from `M` to `N` and a list `l` of elements from `M`.
|
List.sum_nil
theorem List.sum_nil : ∀ {M : Type u_5} [inst : AddZeroClass M], [].sum = 0
This theorem states that for any type `M` that has an additive identity (zero) and a binary addition operation, the sum of an empty list of elements of type `M` is zero. In more mathematical terms, if you consider any set `M` equipped with addition and a zero element (i.e., a set `M` forming an AddZeroClass), the sum over an empty set in `M` is equal to the zero element of `M`.
More concisely: For any AddMonoid `M`, the sum of the empty list of elements from `M` is equal to the additive identity of `M`.
|
List.headI_add_tail_sum
theorem List.headI_add_tail_sum : ∀ (L : List ℕ), L.headI + L.tail.sum = L.sum
This theorem, `List.headI_add_tail_sum`, states that for any list of natural numbers `L`, the sum of the first element (or head) of the list and the sum of the remaining elements (or tail) of the list is equal to the sum of all elements in the list. This theorem assumes the default natural number is `0`.
More concisely: The sum of the head and the sum of the elements in the tail of a list equals the sum of all elements in the list for any list of natural numbers.
|
List.prod_replicate
theorem List.prod_replicate : ∀ {M : Type u_5} [inst : Monoid M] (n : ℕ) (a : M), (List.replicate n a).prod = a ^ n
The theorem states that for any type `M` which forms a Monoid (a mathematical structure with an associative binary operation and an identity element), any natural number `n`, and any element `a` of `M`, the product of a list created by replicating `a` `n` times is equal to `a` raised to the power of `n`. That is, if you create a list by repeating `a` `n` times and then find the product of this list, it will be the same as the monoid operation of `a` with itself `n` times (i.e., `a^n`).
More concisely: For any monoid `M` and natural number `n`, the repeated multiplication of an element `a` in `M` equals the power `a^n` in `M`.
|
List.prod_inv
theorem List.prod_inv :
∀ {G : Type u_9} [inst : CommGroup G] (L : List G), L.prod⁻¹ = (List.map (fun x => x⁻¹) L).prod
This theorem, `List.prod_inv`, is the list version of the `mul_inv` property from group theory. For any given list `L` of elements of a commutative group `G`, the inverse of the product of all elements in `L` is equal to the product of the inverses of all elements in `L`. In mathematical terms, if `G` is a commutative group and `L` is a list of elements in `G`, then $(\prod_{x \in L} x)^{-1} = \prod_{x \in L} x^{-1}$, where the product sign indicates the group operation.
More concisely: For any list `L` of elements in a commutative group `G`, the inverse of the product of all elements in `L` is equal to the product of the inverses of all elements in `L`: $ (\prod\_{x \in L} x)^{-1} = \prod\_{x \in L} x^{-1}$.
|
List.Perm.prod_eq
theorem List.Perm.prod_eq : ∀ {M : Type u_5} [inst : CommMonoid M] {l₁ l₂ : List M}, l₁.Perm l₂ → l₁.prod = l₂.prod
The theorem `List.Perm.prod_eq` states that for any type `α` which is a commutative monoid, if two lists `l₁` and `l₂` of type `α` are permutations of each other, then the product of all elements in `l₁` equals the product of all elements in `l₂`. Here, the product of a list is defined as a sequential multiplication of all elements in the list, starting from 1.
More concisely: For any commutative monoid type `α`, if two lists `l₁` and `l₂` of type `α` are permutations of each other, then the product of their elements is equal.
|
List.get?_zero_add_tail_sum
theorem List.get?_zero_add_tail_sum :
∀ {M : Type u_5} [inst : AddMonoid M] (l : List M), (l.get? 0).getD 0 + l.tail.sum = l.sum
This theorem states that for any list `l` of elements of a type `M` that forms an additive monoid, the sum of the optional value at the zeroth index (or zero if there is no such value) and the sum of the remaining elements in the list is equal to the sum of all the elements in the list. This theorem was formulated this way because the `headI` function, which would normally be used to get the first item of the list, relies on having a default value to return for empty lists, which is not always applicable. Instead, the theorem uses `(l.get? 0).getD 0` to get the first element of the list, or zero if the list is empty.
More concisely: For any additive monoid `M` and list `l` of elements from `M`, the sum of the optional value at index 0 and the sum of the remaining list elements equals the sum of all list elements.
|
List.length_pos_of_prod_lt_one
theorem List.length_pos_of_prod_lt_one :
∀ {M : Type u_5} [inst : Monoid M] [inst_1 : Preorder M] (L : List M), L.prod < 1 → 0 < L.length
This theorem states that for any list of elements, where the type of elements is a monoid and also has a preorder relation, if the product of all elements in this list is less than one, then the list must have a length greater than zero. In simpler terms, a list whose elements multiply to give a value less than one cannot be an empty list.
More concisely: If `M` is a monoid type with a preorder relation such that the product of any non-empty list of elements from `M` has a product strictly less than 1, then the list is non-empty.
|
List.mem_mem_ranges_iff_lt_sum
theorem List.mem_mem_ranges_iff_lt_sum : ∀ (l : List ℕ) {n : ℕ}, (∃ s ∈ l.ranges, n ∈ s) ↔ n < l.sum
This theorem states that for any list `l` of natural numbers and any natural number `n`, `n` is an element of the range of some member of `l` if and only if `n` is strictly less than the sum of all elements in `l`. In other words, a number `n` is in the range of a member of the list when it's smaller than the total sum of all numbers in the list.
More concisely: A natural number `n` is in the range of some number in a list `l` of natural numbers if and only if `n` is strictly less than the sum of all elements in `l`.
|
List.sum_drop_succ
theorem List.sum_drop_succ :
∀ {G : Type u_9} [inst : AddGroup G] (L : List G) (i : ℕ) (p : i < L.length),
(List.drop (i + 1) L).sum = -L.get ⟨i, p⟩ + (List.drop i L).sum
This theorem, `List.sum_drop_succ`, states that for any list `L` of elements of an additive group `G`, and any natural number `i` less than the length of `L`, the sum of the elements obtained by dropping the first `i + 1` elements of `L` is equal to the negation of the `i`th element of `L` added to the sum of the elements obtained by dropping the first `i` elements of `L`. In other words, it's an analogue of the `List.sum_take_succ` theorem for the operation of dropping elements from a list, where the additive inverse operation is present.
More concisely: For any list L of additive group elements and natural number i, the sum of the elements in L starting from the i-th element is equal to the negative of the i-th element plus the sum of the elements in the first i elements of L.
|
List.take_sum_join
theorem List.take_sum_join :
∀ {α : Type u_2} (L : List (List α)) (i : ℕ),
List.take (List.take i (List.map List.length L)).sum L.join = (List.take i L).join
This theorem, `List.take_sum_join`, states that for any list of lists `L` and natural number `i`, when we take the first elements of the joined list `L` up to an index which is the sum of the lengths of the first `i` sublists, we get the same result as when we take the join of the first `i` sublists of `L`. In other words, it asserts equivalence between taking a certain number of elements from a flattened list and joining the same number of initial sublists. Here, `List.take` function is used to obtain the first `i` elements of a list, `List.map List.length L` calculates the lengths of each sublist in `L`, `.sum` adds up these lengths, and `.join` concatenates the lists together.
More concisely: For any list of lists L and natural number i, taking the first i elements from the flattened list obtained by joining the first i sublists of L is equivalent to taking the first i elements from each of the sublists and then concatenating the results.
|
List.prod_set
theorem List.prod_set :
∀ {M : Type u_5} [inst : Monoid M] (L : List M) (n : ℕ) (a : M),
(L.set n a).prod = ((List.take n L).prod * if n < L.length then a else 1) * (List.drop (n + 1) L).prod
The theorem `List.prod_set` states that for any list of elements of monoidal type `M`, replacing an element at position `n` in the list with a new element `a` and then taking the product of the list is the same as taking the product of the first `n` elements of the original list (or all elements if `n` is greater than the length of the list), multiplying it by `a` (or `1` if `n` is greater than or equal to the length of the list), and then multiplying the result by the product of the rest of the elements in original list after position `n`. Therefore, changing a single element in a list does not affect the product of the list elements outside of the new value replacing the old one at the specified index.
More concisely: For any monoidal type `M` and list `ls` of length `n+1`, replacing the `n`-th element of `ls` with `a` preserves the product of `ls`, that is, `ls.take(n) &* a &* ls.drop(n) = ls.take(n+1).product`.
|
List.prod_range_succ'
theorem List.prod_range_succ' :
∀ {M : Type u_5} [inst : Monoid M] (f : ℕ → M) (n : ℕ),
(List.map f (List.range n.succ)).prod = f 0 * (List.map (fun i => f i.succ) (List.range n)).prod
This theorem, named `List.prod_range_succ'`, states that for any type `M` that is an instance of the `Monoid` typeclass, a function `f` from natural numbers to `M`, and a natural number `n`, the product of the list obtained by mapping `f` over the range `0` to `n` (inclusive) is equal to `f(0)` times the product of the list obtained by mapping `f` over the natural numbers from `1` to `n` (inclusive). This essentially pulls off the first term in the product rather than the last, which is a variant of the `prod_range_succ` theorem.
More concisely: For any monoid `M` and function `f` from natural numbers to `M`, the product of the list `[f 0, ..., f n]` is equal to `f 0 * (product [f 1, ..., f n])`.
|
AddMonoidHom.map_list_sum
theorem AddMonoidHom.map_list_sum :
∀ {M : Type u_5} {N : Type u_6} [inst : AddMonoid M] [inst_1 : AddMonoid N] (f : M →+ N) (l : List M),
f l.sum = (List.map (⇑f) l).sum
The theorem `AddMonoidHom.map_list_sum` states that for any list `l` of elements of type `M` in an additive monoid, and any additive monoid homomorphism `f` from `M` to another additive monoid `N`, the result of applying `f` to the sum of the list `l` is equivalent to the sum of the list obtained by mapping `f` over `l`. In mathematical terms, this corresponds to the property ∑ (f(a_i)) = f(∑ a_i) where the sums range over all elements a_i of the list. This theorem is deprecated and `_root_.map_list_sum` should be used instead.
More concisely: For any additive monoid `M`, list `l` of elements from `M`, and additive monoid homomorphism `f` from `M` to another additive monoid `N`, the sum of `f` applied to the elements of `l` equals `f` applied to the sum of `l`. That is, ∑(`f(l)`) = `f`(∑(`l`)).
|
List.sum_range_succ'
theorem List.sum_range_succ' :
∀ {M : Type u_5} [inst : AddMonoid M] (f : ℕ → M) (n : ℕ),
(List.map f (List.range n.succ)).sum = f 0 + (List.map (fun i => f i.succ) (List.range n)).sum
The theorem `List.sum_range_succ'` states that for any type `M` which is an additive monoid, and any function `f` from natural numbers to `M`, for any natural number `n`, the sum of the list obtained by mapping `f` over the range from `0` to `n+1` (`n.succ`), is equal to the sum of `f` applied to `0` and the sum of the list obtained by mapping `f` over the range from `1` (`i.succ`) to `n`. In other words, it rearranges the terms in the sum by moving `f 0` up front.
More concisely: For any additive monoid type `M` and function `f` from natural numbers to `M`, the sum of `[f 0 :: f <$> range (1 :: nat) (succ n) | n]` is equal to `(f 0) + (sum [f x | x <- range (1 :: nat) n])`.
|
map_list_sum
theorem map_list_sum :
∀ {M : Type u_5} {N : Type u_6} [inst : AddMonoid M] [inst_1 : AddMonoid N] {F : Type u_11} [inst_2 : FunLike F M N]
[inst_3 : AddMonoidHomClass F M N] (f : F) (l : List M), f l.sum = (List.map (⇑f) l).sum
This theorem, `map_list_sum`, states that for any two types `M` and `N` that have `AddMonoid` structures, a type `F` that is `FunLike` from `M` to `N` and forms an `AddMonoidHomClass` with `M` and `N`, a function `f` of type `F`, and a list `l` of elements of type `M`, the function `f` applied to the sum of the list `l` is equal to the sum of the list obtained by mapping `f` to every element of `l`. In other words, it states that `f` preserves the sum operation under the map from `M` to `N`. In mathematical notation, it's saying that $f(\sum_{i=1}^{n} l_i) = \sum_{i=1}^{n} f(l_i)$ for a list $l = [l_1, l_2,..., l_n]$ of elements in `M`.
More concisely: For any `FunLike` function `F` from an `AddMonoid` type `M` to an `AddMonoid` type `N` that forms an `AddMonoidHomClass`, and for any list `l` of elements from `M`, the application of `F` to the sum of `l` equals the sum of the images of each element in `l` under `F`. In mathematical notation, `∀[M : AddMonoid, N : AddMonoid, F : AddMonoidHomClass M N, l : List M], F (∑ i, l i) = ∑ i, F i (l i)`.
|
List.Perm.prod_eq'
theorem List.Perm.prod_eq' :
∀ {M : Type u_5} [inst : Monoid M] {l₁ l₂ : List M}, l₁.Perm l₂ → List.Pairwise Commute l₁ → l₁.prod = l₂.prod := by
sorry
The theorem states that, given a type `M` with a monoid structure, if two lists `l₁` and `l₂` of elements of `M` are permutations of each other and all pairs of elements in `l₁` commute (i.e., for any two elements `a` and `b` in `l₁`, `a * b = b * a`), then the product of elements of `l₁` is equal to the product of elements of `l₂`. This implies that the product of a set of elements in a monoid does not depend on the order of the elements if they all commute with each other.
More concisely: Given a monoid `M` and two permutations `l₁` and `l₂` of its elements with the property that all pairs of elements in `l₁` commute, the product of elements in `l₁` is equal to the product of elements in `l₂`.
|
List.sum_singleton
theorem List.sum_singleton : ∀ {M : Type u_5} [inst : AddZeroClass M] {a : M}, [a].sum = a
This theorem states that for any type `M` that has an addition operation and a zero element (a member of the class `AddZeroClass`), the sum of a list that contains only a single element `a` (of type `M`) is `a` itself. In other words, if you have a list with just one element `a`, the sum of all elements in the list is just `a`.
More concisely: For any type `M` in the `AddZeroClass` with addition `+` and zero element `0`, the sum of a list `[a]` containing a single element `a` of type `M` is equal to `a`, i.e., `sum [a] = a`.
|
List.prod_reverse_noncomm
theorem List.prod_reverse_noncomm :
∀ {G : Type u_9} [inst : Group G] (L : List G), L.reverse.prod = (List.map (fun x => x⁻¹) L).prod⁻¹
This theorem, `List.prod_reverse_noncomm`, states a non-commutative variant of the property related to the product of reversed lists. Specifically, for any type `G` that forms a group, and any list `L` of elements from `G`, the product of the elements in the reversed list `L.reverse` is equal to the inverse of the product of the elements in the list obtained by applying the inversion operation to each element of `L`. The operation of applying the inversion is performed using the `List.map` function with the inversion function `\((x) => x^{-1}\)`.
More concisely: For any group `G` and list `L` of elements from `G`, the product of the elements in the reversed list `L.reverse` equals the inverse of the product of the elements in the list `\((\text{map inverse } L)\)`.
|
List.prod_inv_reverse
theorem List.prod_inv_reverse :
∀ {G : Type u_9} [inst : Group G] (L : List G), L.prod⁻¹ = (List.map (fun x => x⁻¹) L).reverse.prod
The theorem `List.prod_inv_reverse` states that for any list `L` of elements from a group `G`, the inverse of the product of elements in `L` is equal to the product of the inverses of elements in `L` taken in reverse order. In mathematical notation, if $L = [g_1, g_2, ..., g_n]$ are elements of a group $G$, then $(g_1g_2...g_n)^{-1} = (g_n^{-1}...g_2^{-1}g_1^{-1})$. This theorem is the list version of the group property that the inverse of the product of two elements is the product of the inverses in reverse order.
More concisely: For any list of group elements `[g\_1, g\_2, ..., g\_n]` in a group `G`, the inverse of their product `g\_1g\_2...g\_n` is equal to the product of their inverses in reverse order `g\_n^(-1)...g\_2^(-1)g\_1^(-1)`.
|
List.sum_reverse_noncomm
theorem List.sum_reverse_noncomm :
∀ {G : Type u_9} [inst : AddGroup G] (L : List G), L.reverse.sum = -(List.map (fun x => -x) L).sum
This is a non-commutative variant of the `List.sum_reverse` theorem. For any type `G` that forms an additive group, the theorem states that the sum of the elements of a reversed list `L : List G` is equal to the negation of the sum of the elements of the list `L` where each element has been negated. In mathematical terms, if `L` is a list of elements in an additive group, then `Σ (reverse(L)) = - Σ (map (λx, -x) L)`. In other words, reversing a list and summing its elements results in the same value as negating each element in the original list, summing them, and then taking the negation.
More concisely: For any additive group `G` and list `L` of its elements, the sum of the reversed list `reverse(L)` equals the negation of the sum of `L` with each element negated: `Σ (reverse(L)) = - Σ (map (λx, -x) L)`.
|
List.sum_append
theorem List.sum_append : ∀ {M : Type u_5} [inst : AddMonoid M] {l₁ l₂ : List M}, (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
sorry
This theorem states that for any type `M` that forms an additive monoid, and for any two lists `l₁` and `l₂` of elements of type `M`, the sum of the elements in the concatenated list `(l₁ ++ l₂)` is equal to the sum of the sums of the elements in `l₁` and `l₂`. In other words, the sum function is distributive over list concatenation. This is analogous to the mathematical property that the sum of a sequence of numbers does not change if the sequence is split into two parts and these parts are summed separately.
More concisely: For any additive monoid type `M`, the sum of elements in the concatenated list `(l₁ ++ l₂)` is equal to the sum of the sums of `l₁` and `l₂`.
|
List.Perm.sum_eq'
theorem List.Perm.sum_eq' :
∀ {M : Type u_5} [inst : AddMonoid M] {l₁ l₂ : List M},
l₁.Perm l₂ → List.Pairwise AddCommute l₁ → l₁.sum = l₂.sum
The theorem `List.Perm.sum_eq'` states that if we have two lists of elements, `l₁` and `l₂`, from a type `M` that is an additive monoid, and if these elements commute with each other additively (meaning for any two elements `a` and `b`, `a + b = b + a`), then if `l₁` is a permutation of `l₂` (i.e., `l₁` and `l₂` contain the same elements but possibly in a different order), the sum of the elements in `l₁` is equal to the sum of the elements in `l₂`. In other words, the theorem asserts that the order in which we add elements does not affect the final sum if the elements commute with each other additively.
More concisely: If `l₁` and `l₂` are permutations of each other from an additive monoid `M` where the elements commute additively, then the sum of `l₁` equals the sum of `l₂`.
|
List.prod_append
theorem List.prod_append : ∀ {M : Type u_5} [inst : Monoid M] {l₁ l₂ : List M}, (l₁ ++ l₂).prod = l₁.prod * l₂.prod
This theorem states that for any type `M` equipped with a monoid structure, and for any two lists `l₁` and `l₂` of elements of type `M`, the product of the elements in the concatenated list `l₁ ++ l₂` is equal to the product of the multiplication of the product of the elements in `l₁` and the product of the elements in `l₂`. In other words, if you compute the product of the elements in two separate lists and then multiply those results together, you get the same result as if you had first concatenated the two lists and then computed the product of all the elements in the combined list. This is essentially saying that the product operation over a list respects the monoid structure of the type of the elements in the list.
More concisely: For any monoid `M` and lists `l₁` and `l₂` of `M`, the product of the concatenated list `l₁ ++ l₂` equals the product of the products of the lists `l₁` and `l₂`. In other words, `∀ (M : Type*) [Monoid M], (∀ i j, m i * m j = m (l₁ ++ l₂) i j)`.
|
List.headI_add_tail_sum_of_ne_nil
theorem List.headI_add_tail_sum_of_ne_nil :
∀ {M : Type u_5} [inst : AddMonoid M] [inst_1 : Inhabited M] (l : List M), l ≠ [] → l.headI + l.tail.sum = l.sum
This theorem, `List.headI_add_tail_sum_of_ne_nil`, asserts that for any non-empty list `l` of elements of a type `M` that forms an additive monoid, the sum of the first element (`headI`) and the sum of the remaining elements (`tail.sum`) equals the sum of all elements in the list (`l.sum`). This avoids the complications that can arise with the `List.headI` function by requiring the list to be non-empty.
More concisely: For any non-empty list `l` of additive monoid elements `M`, the sum of the first element and the sum of the remaining elements equals the sum of all elements in `l`. In other words, `headI l + tail.sum l = l.sum`.
|
List.prod_drop_succ
theorem List.prod_drop_succ :
∀ {G : Type u_9} [inst : Group G] (L : List G) (i : ℕ) (p : i < L.length),
(List.drop (i + 1) L).prod = (L.get ⟨i, p⟩)⁻¹ * (List.drop i L).prod
This theorem, `List.prod_drop_succ`, states that for any list `L` of elements of a group `G` and any natural number `i` less than the length of `L`, the product of the elements in `L` after dropping the first `i+1` elements is equal to the inverse of the `i`th element of `L` multiplied by the product of the elements in `L` after dropping the first `i` elements.
In other words, if you have a list of group elements and you drop one more element from the front of the list, the product of the remaining elements is the same as if you had multiplied the product of the elements obtained by dropping one fewer element by the inverse of the dropped element.
More concisely: For any list `L` of group elements and natural number `i`, the product of the elements in `L` from position `i+1` to the end is equal to the inverse of the `i`th element multiplied by the product of the elements from position `i` to the end.
|
List.headI_mul_tail_prod_of_ne_nil
theorem List.headI_mul_tail_prod_of_ne_nil :
∀ {M : Type u_5} [inst : Monoid M] [inst_1 : Inhabited M] (l : List M), l ≠ [] → l.headI * l.tail.prod = l.prod
This Lean theorem, `List.headI_mul_tail_prod_of_ne_nil`, asserts that for any non-empty list of elements from a monoid `M`, the product of the initial element (`headI`) of the list and the product of the rest of the list (`tail.prod`) is equal to the product of all the elements in the list (`l.prod`). The theorem assumes the existence of a monoid and an inhabited type `M`.
More concisely: For any non-empty list `l` in a monoid `M`, the product of the head `headI` of `l` and the product of the tail `tail` of `l` is equal to the product of all elements in `l`, i.e., `headI * tail.prod = l.prod`.
|
map_list_prod
theorem map_list_prod :
∀ {M : Type u_5} {N : Type u_6} [inst : Monoid M] [inst_1 : Monoid N] {F : Type u_11} [inst_2 : FunLike F M N]
[inst_3 : MonoidHomClass F M N] (f : F) (l : List M), f l.prod = (List.map (⇑f) l).prod
The theorem `map_list_prod` states that for any types `M` and `N` that have monoid structures, any type `F` which is a functor from `M` to `N` and also a monoid homomorphism, and any function `f` of type `F` and any list `l` of type `List M`, the result of applying function `f` to the product of the list `l` is equal to the product of the list obtained by mapping `f` over `l`. In other words, the mapping of a function over the product of a list of monoids is the same as the product of the list obtained by mapping the function over each element of the original list. This theorem essentially asserts the compatibility of the function mapping and product operation in the context of monoids.
More concisely: For any monoid functor F from type M to type N that preserves monoid multiplication, and any list l of monoid elements M, the map of the product of l under F is equal to the product of the images of each element in l under F.
|
List.length_pos_of_sum_pos
theorem List.length_pos_of_sum_pos :
∀ {M : Type u_5} [inst : AddMonoid M] [inst_1 : Preorder M] (L : List M), 0 < L.sum → 0 < L.length
This theorem states that if a list, whose elements belong to some type `M` that forms an additive monoid and for which a preorder relation exists, has a sum greater than zero, then the length of that list must also be greater than zero. In other words, if the summed elements of a list result in a positive value, the list can't be empty.
More concisely: If `M` is an additive monoid with a preorder and a list `ls` over `M` has positive sum, then `ls` is non-empty.
|
List.drop_sum_join
theorem List.drop_sum_join :
∀ {α : Type u_2} (L : List (List α)) (i : ℕ),
List.drop (List.take i (List.map List.length L)).sum L.join = (List.drop i L).join
The theorem `List.drop_sum_join` states that for any list of lists `L` and positive integer `i`, dropping all the elements up to an index, which is the sum of the lengths of the first `i` sublists in `L`, is equivalent to joining the list obtained after dropping the first `i` sublists from `L`. In other words, it says that dropping a certain number of elements from the flattened list is the same as dropping the corresponding sublists from the list of lists before flattening it.
More concisely: For any list of lists `L` and positive integer `i`, the sublist obtained by dropping the first `i` elements from the flattened list `List.flatten L` is equivalent to the concatenation of the first `i` sublists in `L`.
|
List.sum_neg_reverse
theorem List.sum_neg_reverse :
∀ {G : Type u_9} [inst : AddGroup G] (L : List G), -L.sum = (List.map (fun x => -x) L).reverse.sum
This theorem, `List.sum_neg_reverse`, is a version of `add_neg_rev` but for lists. It states that for any given list `L` of elements from an additive group `G`, the negation of the sum of the elements of `L` is equal to the sum of the reversed list obtained by mapping each element of `L` to its negation. Formally, for any list `L` of elements from some additive group `G`, we have `-L.sum = (List.map (fun x => -x) L).reverse.sum`. This theorem thus involves operations of negation, summing over a list, applying a function to each element of a list (`List.map`), and reversing a list.
More concisely: For any additive group `G` and list `L` of elements from `G`, the sum of the negations of the list `L` equals the negation of the sum of the list `L`. In other words, `-sum(L) = sum(map (x : G => -x) L)`.
|
List.sum_take_succ
theorem List.sum_take_succ :
∀ {M : Type u_5} [inst : AddMonoid M] (L : List M) (i : ℕ) (p : i < L.length),
(List.take (i + 1) L).sum = (List.take i L).sum + L.get ⟨i, p⟩
This theorem states that for any list `L` of elements of an additive monoid `M` and any natural number `i` which is less than the length of `L`, the sum of the elements of `L` taken up to the `i+1`th position is equal to the sum of the elements of `L` taken up to the `i`th position plus the `i`th element of `L`. In mathematical terms, for a list `L = [a_0, a_1, ..., a_n]` and `i < n`, we have `sum(a_0, a_1, ..., a_i) = sum(a_0, a_1, ..., a_{i-1}) + a_i`.
More concisely: For any list `L` of additive monoid elements and natural number `i` less than its length, the sum of the first `i+1` elements of `L` equals the sum of the first `i` elements and the `i`-th element of `L`.
|
List.prod_nil
theorem List.prod_nil : ∀ {M : Type u_5} [inst : MulOneClass M], [].prod = 1
This theorem states that the product of an empty list, regardless of what type `M` of elements it might contain, is 1 - provided that `M` is a type for which the operations of multiplication and identity element (one) are defined. Specifically, the `List.prod []` function uses a left fold (`List.foldl`) operation to multiply all elements of the list, starting with the identity element (one). When the list is empty, this function simply returns the starting value, which is 1.
More concisely: The product of an empty list of any type `M` with defined multiplication and identity element is equal to 1.
|
List.length_pos_of_one_lt_prod
theorem List.length_pos_of_one_lt_prod :
∀ {M : Type u_5} [inst : Monoid M] [inst_1 : Preorder M] (L : List M), 1 < L.prod → 0 < L.length
This theorem states that for any list `L` of elements of a certain type `M`, given that `M` is a monoid and there is a defined preorder on `M`, if the product of all elements in `L` is greater than 1, then the length of `L` must be positive. In simpler terms, if multiplying all items in a list gives a result bigger than 1, then the list cannot be empty.
More concisely: If `M` is a monoid with a preorder and `1 < prod L` for any list `L` of `M`, then `L` has a positive length.
|
MonoidHom.map_list_prod
theorem MonoidHom.map_list_prod :
∀ {M : Type u_5} {N : Type u_6} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) (l : List M),
f l.prod = (List.map (⇑f) l).prod
This theorem, which is deprecated and should be replaced with `_root_.map_list_prod`, states that for any monoid homomorphism (`f`) from one monoid (`M`) to another monoid (`N`), the application of `f` to the product of a list of elements in `M` (`List.prod l`) is equal to the product of the list obtained by mapping `f` over `l`. In other words, applying the monoid homomorphism to the product of the list corresponds to taking the product of the list after applying the homomorphism to each of its elements. This theorem showcases the compatibility of the monoid homomorphism with the operation of taking products in the respective monoids.
More concisely: For any monoid homomorphism `f` from monoid `M` to monoid `N`, `f (List.prod l) = List.prod (map f l)`.
|