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 < List.prod l

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 α} : 0 < List.prod l ↔ ∀ x ∈ l, 0 < x

A variant of List.prod_pos for CanonicallyOrderedCommSemiring.