Big operators on a list in ordered groups with zeros

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

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

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

theorem List.prod_map_le_prod_map₀ {R : Type u_1} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulMono R] {ι : Type u_2} {s : List ι} (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 List.prod_map_le_pow_length₀ {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 : List L} (hf0 : ∀ (x : L), x ∈ t → 0 ≤ f x) (hf : ∀ (x : L), x ∈ t → f x ≤ r) : (map (⇑f) t).prod ≤ r ^ t.length

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

theorem List.prod_map_lt_prod_map {R : Type u_1} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulStrictMono R] [NeZero 1] {ι : Type u_2} {s : List ι} (hs : s ≠ []) (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