chore: don't import Field in Algebra.Ring.Equiv (#11881)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib.lean

@@ -153,6 +153,7 @@ import Mathlib.Algebra.Exact
 import Mathlib.Algebra.Expr
 import Mathlib.Algebra.Field.Basic
 import Mathlib.Algebra.Field.Defs
+import Mathlib.Algebra.Field.Equiv
 import Mathlib.Algebra.Field.IsField
 import Mathlib.Algebra.Field.MinimalAxioms
 import Mathlib.Algebra.Field.Opposite

Mathlib/Algebra/Field/Equiv.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2023 Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Junyan Xu
+-/
+import Mathlib.Algebra.Field.IsField
+import Mathlib.Algebra.GroupWithZero.Hom
+
+/-!
+# If a semiring is a field, any isomorphic semiring is also a field.
+
+This is in a separate file to avoiding need to import `Field` in `Mathlib.Algebra.Ring.Equiv.`
+-/
+
+namespace MulEquiv
+
+protected theorem isField {A : Type*} (B : Type*) [Semiring A] [Semiring B] (hB : IsField B)
+    (e : A ≃* B) : IsField A where
+  exists_pair_ne := have ⟨x, y, h⟩ := hB.exists_pair_ne; ⟨e.symm x, e.symm y, e.symm.injective.ne h⟩
+  mul_comm := fun x y => e.injective <| by rw [map_mul, map_mul, hB.mul_comm]
+  mul_inv_cancel := fun h => by
+    obtain ⟨a', he⟩ := hB.mul_inv_cancel ((e.injective.ne h).trans_eq <| map_zero e)
+    exact ⟨e.symm a', e.injective <| by rw [map_mul, map_one, e.apply_symm_apply, he]⟩
+
+end MulEquiv

Mathlib/Algebra/GroupRingAction/Basic.lean

@@ -6,6 +6,7 @@ Authors: Kenny Lau
 import Mathlib.Algebra.GroupWithZero.Units.Lemmas
 import Mathlib.Algebra.Ring.Equiv
 import Mathlib.GroupTheory.GroupAction.Group
+import Mathlib.Algebra.Field.Defs
 
 #align_import algebra.group_ring_action.basic from "leanprover-community/mathlib"@"207cfac9fcd06138865b5d04f7091e46d9320432"
 
@@ -45,7 +46,7 @@ class MulSemiringAction (M : Type u) (R : Type v) [Monoid M] [Semiring R] extend
 section Semiring
 
 variable (M N G : Type*) [Monoid M] [Monoid N] [Group G]
-variable (A R S F : Type v) [AddMonoid A] [Semiring R] [CommSemiring S] [DivisionRing F]
+variable (A R S F : Type v) [AddMonoid A] [Semiring R] [CommSemiring S]
 
 -- note we could not use `extends` since these typeclasses are made with `old_structure_cmd`
 instance (priority := 100) MulSemiringAction.toMulDistribMulAction [h : MulSemiringAction M R] :
@@ -115,6 +116,8 @@ variable {M G A R F}
 
 attribute [simp] smul_one smul_mul' smul_zero smul_add
 
+variable [DivisionRing F]
+
 /-- Note that `smul_inv'` refers to the group case, and `smul_inv` has an additional inverse
 on `x`. -/
 @[simp]

Mathlib/Algebra/Ring/Equiv.lean

@@ -3,7 +3,6 @@ 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 Mathlib.Algebra.Field.IsField
 import Mathlib.Algebra.Group.Opposite
 import Mathlib.Algebra.Group.Units.Equiv
 import Mathlib.Algebra.GroupWithZero.InjSurj
@@ -901,15 +900,8 @@ protected theorem isDomain {A : Type*} (B : Type*) [Semiring A] [Semiring B] [Is
     exists_pair_ne := ⟨e.symm 0, e.symm 1, e.symm.injective.ne zero_ne_one⟩ }
 #noalign ring_equiv.is_domain
 
-protected theorem isField {A : Type*} (B : Type*) [Semiring A] [Semiring B] (hB : IsField B)
-    (e : A ≃* B) : IsField A where
-  exists_pair_ne := have ⟨x, y, h⟩ := hB.exists_pair_ne; ⟨e.symm x, e.symm y, e.symm.injective.ne h⟩
-  mul_comm := fun x y => e.injective <| by rw [map_mul, map_mul, hB.mul_comm]
-  mul_inv_cancel := fun h => by
-    obtain ⟨a', he⟩ := hB.mul_inv_cancel ((e.injective.ne h).trans_eq <| map_zero e)
-    exact ⟨e.symm a', e.injective <| by rw [map_mul, map_one, e.apply_symm_apply, he]⟩
-
 end MulEquiv
 
 -- guard against import creep
+assert_not_exists Field
 assert_not_exists Fintype

Mathlib/RingTheory/Ideal/Basic.lean

@@ -6,6 +6,7 @@ Authors: Kenny Lau, Chris Hughes, Mario Carneiro
 import Mathlib.Tactic.FinCases
 import Mathlib.Data.Nat.Choose.Sum
 import Mathlib.LinearAlgebra.Finsupp
+import Mathlib.Algebra.Field.IsField
 
 #align_import ring_theory.ideal.basic from "leanprover-community/mathlib"@"dc6c365e751e34d100e80fe6e314c3c3e0fd2988"
 

Mathlib/RingTheory/Localization/FractionRing.lean

@@ -5,6 +5,7 @@ Authors: Kenny Lau, Mario Carneiro, Johan Commelin, Amelia Livingston, Anne Baan
 -/
 import Mathlib.Algebra.Algebra.Tower
 import Mathlib.RingTheory.Localization.Basic
+import Mathlib.Algebra.Field.Equiv
 
 #align_import ring_theory.localization.fraction_ring from "leanprover-community/mathlib"@"831c494092374cfe9f50591ed0ac81a25efc5b86"