From 5cd3c25312f210fec96ba1edb2aebfb2ccf2010f Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Thu, 1 Dec 2022 16:53:14 +0000
Subject: [PATCH] chore(algebra/ring/equiv): split out results about big
 operators (#17750)

---
 src/algebra/big_operators/ring_equiv.lean | 45 +++++++++++++++++++++++
 src/algebra/ring/equiv.lean               | 38 ++++---------------
 src/data/matrix/basic.lean                |  3 +-
 3 files changed, 54 insertions(+), 32 deletions(-)
 create mode 100644 src/algebra/big_operators/ring_equiv.lean

diff --git a/src/algebra/big_operators/ring_equiv.lean b/src/algebra/big_operators/ring_equiv.lean
new file mode 100644
index 0000000000000..73d0dd0e43425
--- /dev/null
+++ b/src/algebra/big_operators/ring_equiv.lean
@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2018 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov
+-/
+
+import algebra.big_operators.basic
+import algebra.ring.equiv
+
+/-!
+# Results about mapping big operators across ring equivalences
+-/
+
+namespace ring_equiv
+
+open_locale big_operators
+
+variables {α R S : Type*}
+
+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
+
+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 -/
+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 :=
+unop_map_list_prod f l
+
+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
+
+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
+
+protected lemma map_prod [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) :=
+map_prod g f s
+
+protected lemma map_sum [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) :=
+map_sum g f s
+
+end ring_equiv
diff --git a/src/algebra/ring/equiv.lean b/src/algebra/ring/equiv.lean
index 87083df47e7af..2e33e967e2b2f 100644
--- a/src/algebra/ring/equiv.lean
+++ b/src/algebra/ring/equiv.lean
@@ -3,7 +3,10 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov
 -/
-import algebra.big_operators.basic
+import algebra.group.opposite
+import algebra.hom.ring
+import logic.equiv.set
+import tactic.assert_exists
 
 /-!
 # (Semi)ring equivs
@@ -33,7 +36,6 @@ multiplication in `equiv.perm`, and multiplication in `category_theory.End`, not
 equiv, mul_equiv, add_equiv, ring_equiv, mul_aut, add_aut, ring_aut
 -/
 
-open_locale big_operators
 
 variables {F α β R S S' : Type*}
 
@@ -564,35 +566,6 @@ def of_hom_inv {R S F G : Type*} [non_assoc_semiring R] [non_assoc_semiring S]
 
 end semiring_hom
 
-section big_operators
-
-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
-
-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 -/
-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 :=
-unop_map_list_prod f l
-
-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
-
-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
-
-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) :=
-map_prod g f 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) :=
-map_sum g f s
-
-end big_operators
-
 section group_power
 
 variables [semiring R] [semiring S]
@@ -638,3 +611,6 @@ protected lemma is_domain
   exists_pair_ne := ⟨e.symm 0, e.symm 1, e.symm.injective.ne zero_ne_one⟩ }
 
 end ring_equiv
+
+-- Guard against import creep
+assert_not_exists fintype
diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean
index fa3566f088c5a..e75a25426f29e 100644
--- a/src/data/matrix/basic.lean
+++ b/src/data/matrix/basic.lean
@@ -3,12 +3,13 @@ Copyright (c) 2018 Ellen Arlt. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ellen Arlt, Blair Shi, Sean Leather, Mario Carneiro, Johan Commelin, Lu-Ming Zhang
 -/
+
 import algebra.algebra.basic
 import algebra.big_operators.pi
 import algebra.big_operators.ring
+import algebra.big_operators.ring_equiv
 import algebra.module.linear_map
 import algebra.module.pi
-import algebra.ring.equiv
 import algebra.star.module
 import algebra.star.pi
 import data.fintype.big_operators