Big operators on a list in ordered rings

This file contains the results concerning the interaction of list big operators with ordered rings.

@[simp]

theorem CanonicallyOrderedCommSemiring.list_prod_pos {α : Type u_2} [CanonicallyOrderedCommSemiring α] [Nontrivial α] {l : List α} : 0 < l.prod ↔ ∀ x ∈ l, 0 < x

A variant of List.prod_pos for CanonicallyOrderedCommSemiring.