Big operators on a multiset in ordered groups with zeros

This file contains the results concerning the interaction of multiset big operators with ordered groups with zeros.

theorem Multiset.prod_nonneg {R : Type u_1} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulMono R] {s : Multiset R} (h : ∀ (a : R), a ∈ s → 0 ≤ a) : 0 ≤ s.prod

theorem Multiset.one_le_prod {R : Type u_1} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulMono R] {s : Multiset R} (h : ∀ (a : R), a ∈ s → 1 ≤ a) : 1 ≤ s.prod

theorem Multiset.prod_map_le_prod_map₀ {R : Type u_1} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulMono R] {ι : Type u_2} {s : Multiset ι} (f g : ι → R) (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i) : (map f s).prod ≤ (map g s).prod

theorem Multiset.prod_map_le_pow_card {R : Type u_1} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulMono R] {F : Type u_2} {L : Type u_3} [FunLike F L R] {f : F} {r : R} {t : Multiset L} (hf0 : ∀ (x : L), x ∈ t → 0 ≤ f x) (hf : ∀ (x : L), x ∈ t → f x ≤ r) : (map (⇑f) t).prod ≤ r ^ t.card

theorem Multiset.prod_pos {R : Type u_1} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulStrictMono R] [NeZero 1] {s : Multiset R} (h : ∀ (a : R), a ∈ s → 0 < a) : 0 < s.prod

theorem Multiset.prod_map_lt_prod_map {R : Type u_1} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulStrictMono R] [NeZero 1] {ι : Type u_2} {s : Multiset ι} (hs : s ≠ 0) (f g : ι → R) (h0 : ∀ (i : ι), i ∈ s → 0 < f i) (h : ∀ (i : ι), i ∈ s → f i < g i) : (map f s).prod < (map g s).prod