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} : 0 < m.prod ↔ ∀ (x : R), x ∈ m → 0 < x

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 : α), a ∈ s → p a) : f s.prod ≤ (map f s).prod

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 α) : f s.prod ≤ (map f s).prod

theorem Multiset.mem_le_prod_of_one_le {α : Type u_1} {β : Type u_2} [CommMonoidWithZero β] [PartialOrder β] [PosMulMono β] [ZeroLEOneClass β] {f : α → β} (h1 : ∀ (a : α), 1 ≤ f a) {s : Multiset α} {a : α} (ha : a ∈ s) : f a ≤ (map f s).prod