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 ≤ Multiset.prod s
@[simp]
theorem
CanonicallyOrderedCommSemiring.multiset_prod_pos
{R : Type u_1}
[CanonicallyOrderedCommSemiring R]
[Nontrivial R]
{m : Multiset R}
:
0 < Multiset.prod m ↔ ∀ x ∈ m, 0 < x