chore(algebra/ring/equiv): protect ring equiv lemmas for big operators (

#13624)

src/algebra/ring/equiv.lean

@@ -430,30 +430,30 @@ end semiring_hom
 
 section big_operators
 
-lemma map_list_prod [semiring R] [semiring S] (f : R ≃+* S) (l : list R) :
-  f l.prod = (l.map f).prod := f.to_ring_hom.map_list_prod l
+protected lemma map_list_prod [semiring R] [semiring S] (f : R ≃+* S) (l : list R) :
+  f l.prod = (l.map f).prod := map_list_prod f l
 
-lemma map_list_sum [non_assoc_semiring R] [non_assoc_semiring S] (f : R ≃+* S) (l : list R) :
-  f l.sum = (l.map f).sum := f.to_ring_hom.map_list_sum l
+protected lemma map_list_sum [non_assoc_semiring R] [non_assoc_semiring S] (f : R ≃+* S)
+  (l : list R) : f l.sum = (l.map f).sum := map_list_sum f l
 
 /-- An isomorphism into the opposite ring acts on the product by acting on the reversed elements -/
-lemma unop_map_list_prod [semiring R] [semiring S] (f : R ≃+* Sᵐᵒᵖ) (l : list R) :
+protected lemma unop_map_list_prod [semiring R] [semiring S] (f : R ≃+* Sᵐᵒᵖ) (l : list R) :
   mul_opposite.unop (f l.prod) = (l.map (mul_opposite.unop ∘ f)).reverse.prod :=
-f.to_ring_hom.unop_map_list_prod l
+unop_map_list_prod f l
 
-lemma map_multiset_prod [comm_semiring R] [comm_semiring S] (f : R ≃+* S) (s : multiset R) :
-  f s.prod = (s.map f).prod := f.to_ring_hom.map_multiset_prod s
+protected lemma map_multiset_prod [comm_semiring R] [comm_semiring S] (f : R ≃+* S)
+  (s : multiset R) : f s.prod = (s.map f).prod := map_multiset_prod f s
 
-lemma map_multiset_sum [non_assoc_semiring R] [non_assoc_semiring S]
-  (f : R ≃+* S) (s : multiset R) : f s.sum = (s.map f).sum := f.to_ring_hom.map_multiset_sum s
+protected lemma map_multiset_sum [non_assoc_semiring R] [non_assoc_semiring S]
+  (f : R ≃+* S) (s : multiset R) : f s.sum = (s.map f).sum := map_multiset_sum f s
 
-lemma map_prod {α : Type*} [comm_semiring R] [comm_semiring S] (g : R ≃+* S) (f : α → R)
+protected lemma map_prod {α : Type*} [comm_semiring R] [comm_semiring S] (g : R ≃+* S) (f : α → R)
   (s : finset α) : g (∏ x in s, f x) = ∏ x in s, g (f x) :=
-g.to_ring_hom.map_prod f s
+map_prod g f s
 
-lemma map_sum {α : Type*} [non_assoc_semiring R] [non_assoc_semiring S]
+protected lemma map_sum {α : Type*} [non_assoc_semiring R] [non_assoc_semiring S]
   (g : R ≃+* S) (f : α → R) (s : finset α) : g (∑ x in s, f x) = ∑ x in s, g (f x) :=
-g.to_ring_hom.map_sum f s
+map_sum g f s
 
 end big_operators