# Big operators on a list in ordered rings #

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

source
@[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`.