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 CanonicallyOrderedAdd.list_prod_pos {α : Type u_2} [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [Nontrivial α] {l : List α} : 0 < l.prod ↔ ∀ (x : α), x ∈ l → 0 < x

A variant of List.prod_pos for CanonicallyOrderedAdd.