Big operators on a list in ordered rings #
This file contains the results concerning the interaction of list big operators with ordered rings.
theorem
List.prod_pos
{R : Type u_1}
[StrictOrderedSemiring R]
(l : List R)
(h : ∀ a ∈ l, 0 < a)
:
0 < l.prod
The product of a list of positive natural numbers is positive, and likewise for any nontrivial ordered semiring.
@[simp]
theorem
CanonicallyOrderedCommSemiring.list_prod_pos
{α : Type u_2}
[CanonicallyOrderedCommSemiring α]
[Nontrivial α]
{l : List α}
:
A variant of List.prod_pos for CanonicallyOrderedCommSemiring.