Module docstring
{"# Big operators on a list in ordered rings
This file contains the results concerning the interaction of list big operators with ordered rings. "}
CanonicallyOrderedAdd.list_prod_pos
theorem
{α : Type*} [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [Nontrivial α] :
∀ {l : List α}, 0 < l.prod ↔ (∀ x ∈ l, (0 : α) < x)
Full source
/-- A variant of `List.prod_pos` for `CanonicallyOrderedAdd`. -/
@[simp] lemma CanonicallyOrderedAdd.list_prod_pos {α : Type*}
[CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [Nontrivial α] :
∀ {l : List α}, 0 < l.prod ↔ (∀ x ∈ l, (0 : α) < x)
| [] => by simp
| (x :: xs) => by simp_rw [List.prod_cons, List.forall_mem_cons, CanonicallyOrderedAdd.mul_pos,
list_prod_pos]Informal description
Let $\alpha$ be a nontrivial, canonically ordered additive commutative semiring with no zero divisors. For any list $l$ of elements in $\alpha$, the product of all elements in $l$ is positive if and only if every element in $l$ is positive. In other words, $0 < \prod_{x \in l} x \leftrightarrow \forall x \in l, 0 < x$.