chore(Algebra/BigOperators): delete RingHom.map_* lemmas (#11663)

Mathlib/Algebra/BigOperators/Ring.lean

@@ -6,7 +6,6 @@ Authors: Johannes Hölzl
 import Mathlib.Algebra.BigOperators.Basic
 import Mathlib.Algebra.BigOperators.Multiset.Lemmas
 import Mathlib.Algebra.Field.Defs
-import Mathlib.Algebra.Ring.Opposite
 import Mathlib.Data.Fintype.Powerset
 import Mathlib.Data.Int.Cast.Lemmas
 
@@ -24,57 +23,17 @@ open scoped BigOperators
 
 variable {ι α β γ : Type*} {κ : ι → Type*} {s s₁ s₂ : Finset ι} {i : ι} {a : α} {f g : ι → α}
 
-section Deprecated
-
-#align monoid_hom.map_prod map_prodₓ
-#align add_monoid_hom.map_sum map_sumₓ
-#align mul_equiv.map_prod map_prodₓ
-#align add_equiv.map_sum map_sumₓ
-
-@[deprecated _root_.map_list_prod]
-protected lemma RingHom.map_list_prod [Semiring β] [Semiring γ] (f : β →+* γ) (l : List β) :
-    f l.prod = (l.map f).prod :=
-  map_list_prod f l
-#align ring_hom.map_list_prod RingHom.map_list_prod
-
-@[deprecated _root_.map_list_sum]
-protected lemma RingHom.map_list_sum [NonAssocSemiring β] [NonAssocSemiring γ] (f : β →+* γ)
-    (l : List β) : f l.sum = (l.map f).sum :=
-  map_list_sum f l
-#align ring_hom.map_list_sum RingHom.map_list_sum
-
-/-- A morphism into the opposite ring acts on the product by acting on the reversed elements. -/
-@[deprecated _root_.unop_map_list_prod]
-protected lemma RingHom.unop_map_list_prod [Semiring β] [Semiring γ] (f : β →+* γᵐᵒᵖ)
-    (l : List β) : MulOpposite.unop (f l.prod) = (l.map (MulOpposite.unop ∘ f)).reverse.prod :=
-  unop_map_list_prod f l
-#align ring_hom.unop_map_list_prod RingHom.unop_map_list_prod
-
-@[deprecated _root_.map_multiset_prod]
-protected lemma RingHom.map_multiset_prod [CommSemiring β] [CommSemiring γ] (f : β →+* γ)
-    (s : Multiset β) : f s.prod = (s.map f).prod :=
-  map_multiset_prod f s
-#align ring_hom.map_multiset_prod RingHom.map_multiset_prod
-
-@[deprecated _root_.map_multiset_sum]
-protected lemma RingHom.map_multiset_sum [NonAssocSemiring β] [NonAssocSemiring γ] (f : β →+* γ)
-    (s : Multiset β) : f s.sum = (s.map f).sum :=
-  map_multiset_sum f s
-#align ring_hom.map_multiset_sum RingHom.map_multiset_sum
-
-@[deprecated _root_.map_prod]
-protected lemma RingHom.map_prod [CommSemiring β] [CommSemiring γ] (g : β →+* γ) (f : α → β)
-    (s : Finset α) : g (∏ x in s, f x) = ∏ x in s, g (f x) :=
-  map_prod g f s
-#align ring_hom.map_prod RingHom.map_prod
-
-@[deprecated _root_.map_sum]
-protected lemma RingHom.map_sum [NonAssocSemiring β] [NonAssocSemiring γ] (g : β →+* γ)
-    (f : α → β) (s : Finset α) : g (∑ x in s, f x) = ∑ x in s, g (f x) :=
-  map_sum g f s
-#align ring_hom.map_sum RingHom.map_sum
-
-end Deprecated
+#align monoid_hom.map_prod map_prod
+#align add_monoid_hom.map_sum map_sum
+#align mul_equiv.map_prod map_prod
+#align add_equiv.map_sum map_sum
+#align ring_hom.map_list_prod map_list_prod
+#align ring_hom.map_list_sum map_list_sum
+#align ring_hom.unop_map_list_prod unop_map_list_prod
+#align ring_hom.map_multiset_prod map_multiset_prod
+#align ring_hom.map_multiset_sum map_multiset_sum
+#align ring_hom.map_prod map_prod
+#align ring_hom.map_sum map_sum
 
 namespace Finset
 

Mathlib/Algebra/BigOperators/RingEquiv.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov
 import Mathlib.Algebra.BigOperators.Basic
 import Mathlib.Algebra.BigOperators.List.Lemmas
 import Mathlib.Algebra.Ring.Equiv
+import Mathlib.Algebra.Ring.Opposite
 
 #align_import algebra.big_operators.ring_equiv from "leanprover-community/mathlib"@"008205aa645b3f194c1da47025c5f110c8406eab"
 

Mathlib/Algebra/CharP/ExpChar.lean

@@ -335,19 +335,19 @@ theorem coe_iterateFrobenius_mul : iterateFrobenius R p (m * n) = (iterateFroben
 variable {R}
 
 theorem frobenius_mul : frobenius R p (x * y) = frobenius R p x * frobenius R p y :=
-  (frobenius R p).map_mul x y
+  map_mul (frobenius R p) x y
 #align frobenius_mul frobenius_mul
 
 theorem frobenius_one : frobenius R p 1 = 1 :=
   one_pow _
 #align frobenius_one frobenius_one
 
 theorem MonoidHom.map_frobenius : f (frobenius R p x) = frobenius S p (f x) :=
-  f.map_pow x p
+  map_pow f x p
 #align monoid_hom.map_frobenius MonoidHom.map_frobenius
 
 theorem RingHom.map_frobenius : g (frobenius R p x) = frobenius S p (g x) :=
-  g.map_pow x p
+  map_pow g x p
 #align ring_hom.map_frobenius RingHom.map_frobenius
 
 theorem MonoidHom.map_iterate_frobenius (n : ℕ) :
@@ -406,30 +406,30 @@ open BigOperators
 variable {R}
 
 theorem list_sum_pow_char (l : List R) : l.sum ^ p = (l.map (· ^ p : R → R)).sum :=
-  (frobenius R p).map_list_sum _
+  map_list_sum (frobenius R p) _
 #align list_sum_pow_char list_sum_pow_char
 
 theorem multiset_sum_pow_char (s : Multiset R) : s.sum ^ p = (s.map (· ^ p : R → R)).sum :=
-  (frobenius R p).map_multiset_sum _
+  map_multiset_sum (frobenius R p) _
 #align multiset_sum_pow_char multiset_sum_pow_char
 
 theorem sum_pow_char {ι : Type*} (s : Finset ι) (f : ι → R) :
     (∑ i in s, f i) ^ p = ∑ i in s, f i ^ p :=
-  (frobenius R p).map_sum _ _
+  map_sum (frobenius R p) _ _
 #align sum_pow_char sum_pow_char
 
 variable (n : ℕ)
 
 theorem list_sum_pow_char_pow (l : List R) : l.sum ^ p ^ n = (l.map (· ^ p ^ n : R → R)).sum :=
-  (iterateFrobenius R p n).map_list_sum _
+  map_list_sum (iterateFrobenius R p n) _
 
 theorem multiset_sum_pow_char_pow (s : Multiset R) :
     s.sum ^ p ^ n = (s.map (· ^ p ^ n : R → R)).sum :=
-  (iterateFrobenius R p n).map_multiset_sum _
+  map_multiset_sum (iterateFrobenius R p n) _
 
 theorem sum_pow_char_pow {ι : Type*} (s : Finset ι) (f : ι → R) :
     (∑ i in s, f i) ^ p ^ n = ∑ i in s, f i ^ p ^ n :=
-  (iterateFrobenius R p n).map_sum _ _
+  map_sum (iterateFrobenius R p n) _ _
 
 end CommSemiring
 
@@ -438,11 +438,11 @@ section CommRing
 variable [CommRing R] (p : ℕ) [ExpChar R p] (x y : R)
 
 theorem frobenius_neg : frobenius R p (-x) = -frobenius R p x :=
-  (frobenius R p).map_neg x
+  map_neg ..
 #align frobenius_neg frobenius_neg
 
 theorem frobenius_sub : frobenius R p (x - y) = frobenius R p x - frobenius R p y :=
-  (frobenius R p).map_sub x y
+  map_sub ..
 #align frobenius_sub frobenius_sub
 
 end CommRing

Mathlib/Algebra/GeomSum.lean

@@ -9,6 +9,7 @@ import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Data.Nat.Parity
 import Mathlib.Tactic.Abel
+import Mathlib.Algebra.Ring.Opposite
 
 #align_import algebra.geom_sum from "leanprover-community/mathlib"@"f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c"
 

Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

@@ -8,6 +8,7 @@ import Mathlib.GroupTheory.Submonoid.Operations
 import Mathlib.GroupTheory.Submonoid.Membership
 import Mathlib.GroupTheory.Submonoid.MulOpposite
 import Mathlib.GroupTheory.GroupAction.Opposite
+import Mathlib.Algebra.Ring.Opposite
 
 #align_import ring_theory.non_zero_divisors from "leanprover-community/mathlib"@"1126441d6bccf98c81214a0780c73d499f6721fe"
 

Mathlib/Data/NNRat/BigOperators.lean

@@ -17,27 +17,27 @@ namespace NNRat
 
 @[norm_cast]
 theorem coe_list_sum (l : List ℚ≥0) : (l.sum : ℚ) = (l.map (↑)).sum :=
-  coeHom.map_list_sum _
+  map_list_sum coeHom _
 #align nnrat.coe_list_sum NNRat.coe_list_sum
 
 @[norm_cast]
 theorem coe_list_prod (l : List ℚ≥0) : (l.prod : ℚ) = (l.map (↑)).prod :=
-  coeHom.map_list_prod _
+  map_list_prod coeHom _
 #align nnrat.coe_list_prod NNRat.coe_list_prod
 
 @[norm_cast]
 theorem coe_multiset_sum (s : Multiset ℚ≥0) : (s.sum : ℚ) = (s.map (↑)).sum :=
-  coeHom.map_multiset_sum _
+  map_multiset_sum coeHom _
 #align nnrat.coe_multiset_sum NNRat.coe_multiset_sum
 
 @[norm_cast]
 theorem coe_multiset_prod (s : Multiset ℚ≥0) : (s.prod : ℚ) = (s.map (↑)).prod :=
-  coeHom.map_multiset_prod _
+  map_multiset_prod coeHom _
 #align nnrat.coe_multiset_prod NNRat.coe_multiset_prod
 
 @[norm_cast]
 theorem coe_sum {s : Finset α} {f : α → ℚ≥0} : ↑(∑ a in s, f a) = ∑ a in s, (f a : ℚ) :=
-  coeHom.map_sum _ _
+  map_sum coeHom _ _
 #align nnrat.coe_sum NNRat.coe_sum
 
 theorem toNNRat_sum_of_nonneg {s : Finset α} {f : α → ℚ} (hf : ∀ a, a ∈ s → 0 ≤ f a) :
@@ -48,7 +48,7 @@ theorem toNNRat_sum_of_nonneg {s : Finset α} {f : α → ℚ} (hf : ∀ a, a 
 
 @[norm_cast]
 theorem coe_prod {s : Finset α} {f : α → ℚ≥0} : ↑(∏ a in s, f a) = ∏ a in s, (f a : ℚ) :=
-  coeHom.map_prod _ _
+  map_prod coeHom _ _
 #align nnrat.coe_prod NNRat.coe_prod
 
 theorem toNNRat_prod_of_nonneg {s : Finset α} {f : α → ℚ} (hf : ∀ a ∈ s, 0 ≤ f a) :

Mathlib/Data/Real/NNReal.lean

@@ -308,27 +308,27 @@ theorem coe_zpow (r : ℝ≥0) (n : ℤ) : ((r ^ n : ℝ≥0) : ℝ) = (r : ℝ)
 
 @[norm_cast]
 theorem coe_list_sum (l : List ℝ≥0) : ((l.sum : ℝ≥0) : ℝ) = (l.map (↑)).sum :=
-  toRealHom.map_list_sum l
+  map_list_sum toRealHom l
 #align nnreal.coe_list_sum NNReal.coe_list_sum
 
 @[norm_cast]
 theorem coe_list_prod (l : List ℝ≥0) : ((l.prod : ℝ≥0) : ℝ) = (l.map (↑)).prod :=
-  toRealHom.map_list_prod l
+  map_list_prod toRealHom l
 #align nnreal.coe_list_prod NNReal.coe_list_prod
 
 @[norm_cast]
 theorem coe_multiset_sum (s : Multiset ℝ≥0) : ((s.sum : ℝ≥0) : ℝ) = (s.map (↑)).sum :=
-  toRealHom.map_multiset_sum s
+  map_multiset_sum toRealHom s
 #align nnreal.coe_multiset_sum NNReal.coe_multiset_sum
 
 @[norm_cast]
 theorem coe_multiset_prod (s : Multiset ℝ≥0) : ((s.prod : ℝ≥0) : ℝ) = (s.map (↑)).prod :=
-  toRealHom.map_multiset_prod s
+  map_multiset_prod toRealHom s
 #align nnreal.coe_multiset_prod NNReal.coe_multiset_prod
 
 @[norm_cast]
 theorem coe_sum {α} {s : Finset α} {f : α → ℝ≥0} : ↑(∑ a in s, f a) = ∑ a in s, (f a : ℝ) :=
-  toRealHom.map_sum _ _
+  map_sum toRealHom _ _
 #align nnreal.coe_sum NNReal.coe_sum
 
 theorem _root_.Real.toNNReal_sum_of_nonneg {α} {s : Finset α} {f : α → ℝ}
@@ -340,7 +340,7 @@ theorem _root_.Real.toNNReal_sum_of_nonneg {α} {s : Finset α} {f : α → ℝ}
 
 @[norm_cast]
 theorem coe_prod {α} {s : Finset α} {f : α → ℝ≥0} : ↑(∏ a in s, f a) = ∏ a in s, (f a : ℝ) :=
-  toRealHom.map_prod _ _
+  map_prod toRealHom _ _
 #align nnreal.coe_prod NNReal.coe_prod
 
 theorem _root_.Real.toNNReal_prod_of_nonneg {α} {s : Finset α} {f : α → ℝ}