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 ∈ 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 ∈ 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 : ι → R) (g : ι → R) (h0 : ∀ i ∈ s, 0 ≤ f i) (h : ∀ i ∈ s, f i ≤ g i) : (List.map f s).prod ≤ (List.map g s).prod

theorem List.prod_pos {R : Type u_1} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulStrictMono R] [NeZero 1] {s : List R} (h : ∀ 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 : ι → R) (g : ι → R) (h0 : ∀ i ∈ s, 0 < f i) (h : ∀ i ∈ s, f i < g i) : (List.map f s).prod < (List.map g s).prod