Big operators on a multiset in ordered rings #
This file contains the results concerning the interaction of multiset big operators with ordered rings.
@[simp]
theorem
CanonicallyOrderedAdd.multiset_prod_pos
{R : Type u_1}
[CommSemiring R]
[PartialOrder R]
[CanonicallyOrderedAdd R]
[NoZeroDivisors R]
[Nontrivial R]
{m : Multiset R}
: