List.prod_eq_zero
theorem List.prod_eq_zero : ∀ {M₀ : Type u_6} [inst : MonoidWithZero M₀] {L : List M₀}, 0 ∈ L → L.prod = 0
This theorem states that if zero is an element of a list `L` of elements from a type `M₀` that forms a monoid with zero, then the product of all elements in the list `L` equals zero. In the special case where `M₀` is a nontrivial monoid with zero and no divisors, this statement can be strengthened to an `if and only if` condition, which is covered by the theorem `List.prod_eq_zero_iff`.
More concisely: If `M₀` is a monoid with zero and zero is an element of list `L` of `M₀`, then the product of all elements in `L` equals zero. (In the special case where `M₀` is a nontrivial monoid with zero and no divisors, this is equivalent to `L` containing zero.)
|
MonoidHom.unop_map_list_prod
theorem MonoidHom.unop_map_list_prod :
∀ {M : Type u_3} {N : Type u_4} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* Nᵐᵒᵖ) (l : List M),
(f l.prod).unop = (List.map (MulOpposite.unop ∘ ⇑f) l).reverse.prod
The theorem `MonoidHom.unop_map_list_prod` states that for any monoids `M` and `N`, and any morphism `f` from `M` to the opposite monoid of `N`, when `f` is applied to the product of a list `l` of elements from `M` and the result is unoped (i.e., converted back from the opposite monoid), it equals the product of the reverse of the list obtained by mapping each element of `l` to `N` using `f`, and then applying `unop`. In other words, a morphism into the opposite monoid acts on the product of a list by acting on the reversed elements of the list.
More concisely: For any monoids M and N, and any morphism f from M to the opposite monoid of N, applying f to the product of a list l of elements from M and then unoping the result equals the product of the reverse of the list obtained by applying f to each element of l in the opposite monoid.
|
List.dvd_prod
theorem List.dvd_prod : ∀ {M : Type u_3} [inst : CommMonoid M] {a : M} {l : List M}, a ∈ l → a ∣ l.prod
This theorem, `List.dvd_prod`, states that for any commutative monoid `M`, given an element `a` of `M` and a list `l` of elements of `M`, if `a` is a member of `l`, then `a` divides the product of all elements in the list `l`. In mathematical terms, if $a \in l$, then $a$ divides $\prod_{i=1}^{n} l_i$, where $l_i$ are the elements of the list `l`.
More concisely: If `a` is an element of a list `l` of commutative monoid elements, then `a` divides the product of all elements in `l`. In mathematical notation, if $a \in l$ and $l$ is a list of commutative monoid elements, then $a \mid \prod\_{i=1}^{n} l\_i$.
|
unop_map_list_prod
theorem unop_map_list_prod :
∀ {M : Type u_3} {N : Type u_4} [inst : Monoid M] [inst_1 : Monoid N] {F : Type u_9} [inst_2 : FunLike F M Nᵐᵒᵖ]
[inst_3 : MonoidHomClass F M Nᵐᵒᵖ] (f : F) (l : List M),
(f l.prod).unop = (List.map (MulOpposite.unop ∘ ⇑f) l).reverse.prod
The theorem `unop_map_list_prod` states that for any two monoids `M` and `N`, a function `F` that is a homomorphism from `M` to the opposite monoid of `N`, and a list `l` of elements of `M`, the application of the function `F` to the product of the elements in `l`, when unop'ed (i.e., converted back from the opposite monoid), gives the same result as the product of the reversed list obtained by mapping the unop'ed function `F` over `l`. In simpler terms, it states that a morphism into the opposite monoid affects the product of a list of monoid elements by acting on the elements in the reversed order.
More concisely: For any monoids M and N, a homomorphism F from M to the opposite monoid of N preserves the product of lists, that is, F (prod xs) = prod (reverse (map F (unop xs))) where unop denotes the operation of converting an element from the opposite monoid back to the original monoid.
|
List.neg_one_mem_of_prod_eq_neg_one
theorem List.neg_one_mem_of_prod_eq_neg_one : ∀ {l : List ℤ}, l.prod = -1 → -1 ∈ l
This theorem states that if the product of a list of integers equals `-1`, then at least one element in that list must be `-1`. In other words, it's impossible to obtain a product of `-1` from a list of integers without including `-1` as one of the integers in the list.
More concisely: If the product of a list of integers is `-1`, then the list contains an `-1`.
|
List.length_le_sum_of_one_le
theorem List.length_le_sum_of_one_le : ∀ (L : List ℕ), (∀ i ∈ L, 1 ≤ i) → L.length ≤ L.sum
This theorem states that if every element in a list of natural numbers is at least `1`, then the length of the list is less than or equal to the sum of the elements in the list. In other words, if you have a list where every number is `1` or greater, adding up all the numbers will give you a total that's at least as big as the number of items on the list.
More concisely: If `X` is a list of natural numbers where every element is greater than or equal to `1`, then the length of `X` is less than or equal to the sum of its elements.
|
List.prod_eq_zero_iff
theorem List.prod_eq_zero_iff :
∀ {M₀ : Type u_6} [inst : MonoidWithZero M₀] [inst_1 : Nontrivial M₀] [inst_2 : NoZeroDivisors M₀] {L : List M₀},
L.prod = 0 ↔ 0 ∈ L
This theorem states that for a list `L` of elements of type `M₀`, where `M₀` is a monoid with zero, nontrivial, and with no zero divisors, the product of the elements of `L` is zero if and only if zero is an element of `L`. In other words, the combined multiplication of all elements in the list `L` results in zero specifically when the list `L` contains at least one zero. The theorem also refers to `List.prod_eq_zero` for a similar statement that requires less restrictive assumptions on the type `M₀`.
More concisely: For a list of elements from a monoid `M₀` with no zero divisors and a zero element, the product of the list is zero if and only if the list contains the zero element.
|
List.prod_ne_zero
theorem List.prod_ne_zero :
∀ {M₀ : Type u_6} [inst : MonoidWithZero M₀] [inst_1 : Nontrivial M₀] [inst_2 : NoZeroDivisors M₀] {L : List M₀},
0 ∉ L → L.prod ≠ 0
This theorem states that for any type `M₀` which is a non-trivial monoid with zero and no zero divisors (i.e., the multiplication of any two non-zero elements of `M₀` is never zero), the product of any list `L` of elements of `M₀` is never zero, given the condition that the element zero does not belong to `L`. Here, "non-trivial" means that there exists at least one element in `M₀` which is not equal to zero, while "monoid with zero" is a mathematical structure that includes an operation that is associative, an identity element (which is zero in this case), and every element having an inverse with respect to this identity.
More concisely: If `M₀` is a non-trivial monoid with zero and no zero divisors, then the product of any finite list of non-zero elements from `M₀` is non-zero.
|