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}
:
theorem
Multiset.le_prod_of_submultiplicative_on_pred_of_nonneg
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[CommMonoidWithZero β]
[PartialOrder β]
[PosMulMono β]
(f : α → β)
(p : α → Prop)
(h0 : ∀ (a : α), 0 ≤ f a)
(h_one : f 1 ≤ 1)
(h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b)
(hp_mul : ∀ (a b : α), p a → p b → p (a * b))
(s : Multiset α)
(hps : ∀ a ∈ s, p a)
:
theorem
Multiset.le_prod_of_submultiplicative_of_nonneg
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
[CommMonoidWithZero β]
[PartialOrder β]
[PosMulMono β]
(f : α → β)
(h0 : ∀ (a : α), 0 ≤ f a)
(h_one : f 1 ≤ 1)
(h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b)
(s : Multiset α)
: