Finset.sup in a group with zero

theorem Finset.sup_mul_le_mul_sup_of_nonneg {ι : Type u_1} {M₀ : Type u_2} [MonoidWithZero M₀] {s : Finset ι} {a b : ι → M₀} [SemilatticeSup M₀] [OrderBot M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) : s.sup (a * b) ≤ s.sup a * s.sup b

theorem Finset.mul_inf_le_inf_mul_of_nonneg {ι : Type u_1} {M₀ : Type u_2} [MonoidWithZero M₀] {s : Finset ι} {a b : ι → M₀} [SemilatticeInf M₀] [OrderTop M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) : s.inf a * s.inf b ≤ s.inf (a * b)

theorem Finset.sup'_mul_le_mul_sup'_of_nonneg {ι : Type u_1} {M₀ : Type u_2} [MonoidWithZero M₀] {s : Finset ι} {a b : ι → M₀} [SemilatticeSup M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) (hs : s.Nonempty) : s.sup' hs (a * b) ≤ s.sup' hs a * s.sup' hs b

theorem Finset.inf'_mul_le_mul_inf'_of_nonneg {ι : Type u_1} {M₀ : Type u_2} [MonoidWithZero M₀] {s : Finset ι} {a b : ι → M₀} [SemilatticeInf M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) (hs : s.Nonempty) : s.inf' hs a * s.inf' hs b ≤ s.inf' hs (a * b)

theorem Finset.sup'_mul₀ {ι : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] [SemilatticeSup G₀] {a : G₀} [MulPosReflectLT G₀] (ha : 0 ≤ a) (f : ι → G₀) (s : Finset ι) (hs : s.Nonempty) : s.sup' hs f * a = s.sup' hs fun (i : ι) => f i * a

theorem Finset.mul₀_sup' {ι : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] [SemilatticeSup G₀] {a : G₀} [PosMulReflectLT G₀] (ha : 0 ≤ a) (f : ι → G₀) (s : Finset ι) (hs : s.Nonempty) : a * s.sup' hs f = s.sup' hs fun (i : ι) => a * f i

theorem Finset.sup'_div₀ {ι : Type u_1} {G₀ : Type u_3} [GroupWithZero G₀] [SemilatticeSup G₀] {a : G₀} [MulPosReflectLT G₀] (ha : 0 ≤ a) (f : ι → G₀) (s : Finset ι) (hs : s.Nonempty) : s.sup' hs f / a = s.sup' hs fun (i : ι) => f i / a

theorem Finset.sup_div₀ {ι : Type u_1} {G₀ : Type u_3} [LinearOrderedCommGroupWithZero G₀] {a : G₀} (ha : 0 ≤ a) (s : Finset ι) (f : ι → G₀) : s.sup f / a = s.sup fun (i : ι) => f i / a