chore(Algebra/Order/BigOperators): move lemmas which don't use addition out of Ring/

Author: b-mehta

Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.BigOperators.Ring.Finset
 public import Mathlib.Algebra.Order.AbsoluteValue.Basic
 public import Mathlib.Algebra.Order.BigOperators.Group.Finset
+public import Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
 public import Mathlib.Algebra.Order.BigOperators.Ring.Multiset
 public import Mathlib.Tactic.Ring
 
@@ -27,66 +28,6 @@ variable {ι R S : Type*}
 
 namespace Finset
 
-section CommMonoidWithZero
-variable [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R]
-
-section PosMulMono
-variable [PosMulMono R] {f g : ι → R} {s t : Finset ι}
-
-lemma prod_nonneg (h0 : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ ∏ i ∈ s, f i :=
-  prod_induction f (fun i ↦ 0 ≤ i) (fun _ _ ha hb ↦ mul_nonneg ha hb) zero_le_one h0
-
-/-- If all `f i`, `i ∈ s`, are nonnegative and each `f i` is less than or equal to `g i`, then the
-product of `f i` is less than or equal to the product of `g i`. See also `Finset.prod_le_prod'` for
-the case of an ordered commutative multiplicative monoid. -/
-@[gcongr]
-lemma prod_le_prod (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i) :
-    ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i := by
-  induction s using Finset.cons_induction with
-  | empty => simp
-  | cons a s has ih =>
-    simp only [prod_cons, forall_mem_cons] at h0 h1 ⊢
-    have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
-    gcongr
-    exacts [prod_nonneg h0.2, h0.1.trans h1.1, h1.1, ih h0.2 h1.2]
-
-/-- If each `f i`, `i ∈ s` belongs to `[0, 1]`, then their product is less than or equal to one.
-See also `Finset.prod_le_one'` for the case of an ordered commutative multiplicative monoid. -/
-lemma prod_le_one (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ 1) : ∏ i ∈ s, f i ≤ 1 := by
-  convert ← prod_le_prod h0 h1
-  exact Finset.prod_const_one
-
-end PosMulMono
-
-section PosMulStrictMono
-variable [PosMulStrictMono R] [Nontrivial R] {f g : ι → R} {s t : Finset ι}
-
-lemma prod_pos (h0 : ∀ i ∈ s, 0 < f i) : 0 < ∏ i ∈ s, f i :=
-  prod_induction f (fun x ↦ 0 < x) (fun _ _ ha hb ↦ mul_pos ha hb) zero_lt_one h0
-
-lemma prod_lt_prod (hf : ∀ i ∈ s, 0 < f i) (hfg : ∀ i ∈ s, f i ≤ g i)
-    (hlt : ∃ i ∈ s, f i < g i) :
-    ∏ i ∈ s, f i < ∏ i ∈ s, g i := by
-  classical
-  obtain ⟨i, hi, hilt⟩ := hlt
-  rw [← insert_erase hi, prod_insert (notMem_erase _ _), prod_insert (notMem_erase _ _)]
-  have := posMulStrictMono_iff_mulPosStrictMono.1 ‹PosMulStrictMono R›
-  refine mul_lt_mul_of_pos_of_nonneg' hilt ?_ ?_ ?_
-  · exact prod_le_prod (fun j hj => le_of_lt (hf j (mem_of_mem_erase hj)))
-      (fun _ hj ↦ hfg _ <| mem_of_mem_erase hj)
-  · exact prod_pos fun j hj => hf j (mem_of_mem_erase hj)
-  · exact (hf i hi).le.trans hilt.le
-
-lemma prod_lt_prod_of_nonempty (hf : ∀ i ∈ s, 0 < f i) (hfg : ∀ i ∈ s, f i < g i)
-    (h_ne : s.Nonempty) :
-    ∏ i ∈ s, f i < ∏ i ∈ s, g i := by
-  apply prod_lt_prod hf fun i hi => le_of_lt (hfg i hi)
-  obtain ⟨i, hi⟩ := h_ne
-  exact ⟨i, hi, hfg i hi⟩
-
-end PosMulStrictMono
-end CommMonoidWithZero
-
 section OrderedSemiring
 
 variable [Semiring R] [PartialOrder R] [IsOrderedRing R] {f : ι → R} {s : Finset ι}