CanonicallyOrderedCommSemiring.list_prod_pos
theorem CanonicallyOrderedCommSemiring.list_prod_pos :
∀ {α : Type u_2} [inst : CanonicallyOrderedCommSemiring α] [inst_1 : Nontrivial α] {l : List α},
0 < l.prod ↔ ∀ x ∈ l, 0 < x
This theorem, `CanonicallyOrderedCommSemiring.list_prod_pos`, states that for any type `α` that is a `CanonicallyOrderedCommSemiring` and `Nontrivial`, the product of a list `l` of `α` is greater than zero if and only if every element `x` in the list `l` is greater than zero. In other words, the product of all elements in the list is positive if all elements in the list are positive, under the conditions that the elements belong to a canonically ordered commutative semiring and the semiring is nontrivial (i.e., it contains at least two distinct elements).
More concisely: Given a `CanonicallyOrderedCommSemiring` α that is `Nontrivial`, the product of a list of α's is positive if and only if all elements in the list are positive.
|
List.prod_pos
theorem List.prod_pos : ∀ {R : Type u_1} [inst : StrictOrderedSemiring R] (l : List R), (∀ a ∈ l, 0 < a) → 0 < l.prod
This theorem states that for any list of positive numbers in a strictly ordered semiring (a type of algebraic structure that includes operations analogous to addition and multiplication), the product of all numbers in the list is also positive. This theorem applies to any list of positive natural numbers and can be extended to any nontrivial ordered semiring.
More concisely: In a strictly ordered semiring, the product of any list of positive elements is positive.
|