Big operators on a multiset in ordered rings

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

theorem Multiset.prod_nonneg {R : Type u_1} [OrderedCommSemiring R] {s : Multiset R} (h : ∀ a ∈ s, 0 ≤ a) : 0 ≤ s.prod

@[simp]

theorem CanonicallyOrderedCommSemiring.multiset_prod_pos {R : Type u_1} [CanonicallyOrderedCommSemiring R] [Nontrivial R] {m : Multiset R} : 0 < m.prod ↔ ∀ x ∈ m, 0 < x