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
CanonicallyOrderedCommSemiring.multiset_prod_pos
{R : Type u_1}
[CanonicallyOrderedCommSemiring R]
[Nontrivial R]
{m : Multiset R}
: