chore(Data/ZMod/Basic): don't import Field

Mathlib.lean

@@ -240,12 +240,14 @@ import Mathlib.Algebra.Field.Defs
 import Mathlib.Algebra.Field.Equiv
 import Mathlib.Algebra.Field.IsField
 import Mathlib.Algebra.Field.MinimalAxioms
+import Mathlib.Algebra.Field.NegOnePow
 import Mathlib.Algebra.Field.Opposite
 import Mathlib.Algebra.Field.Power
 import Mathlib.Algebra.Field.Rat
 import Mathlib.Algebra.Field.Subfield.Basic
 import Mathlib.Algebra.Field.Subfield.Defs
 import Mathlib.Algebra.Field.ULift
+import Mathlib.Algebra.Field.ZMod
 import Mathlib.Algebra.Free
 import Mathlib.Algebra.FreeAlgebra
 import Mathlib.Algebra.FreeAlgebra.Cardinality

Mathlib/Algebra/Field/NegOnePow.lean

@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2023 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou, Johan Commelin
+-/
+import Mathlib.Algebra.Field.Defs
+import Mathlib.Algebra.Ring.NegOnePow
+import Mathlib.Tactic.NormNum
+
+/-! # Integer powers of `-1` in a field -/
+
+namespace Int
+
+lemma cast_negOnePow (K : Type*) (n : ℤ) [Field K] : n.negOnePow = (-1 : K) ^ n := by
+  rcases even_or_odd' n with ⟨k, rfl | rfl⟩
+  · simp [zpow_mul, zpow_ofNat]
+  · rw [zpow_add_one₀ (by norm_num), zpow_mul, zpow_ofNat]
+    simp
+
+@[deprecated (since := "2024-10-20")] alias coe_negOnePow := cast_negOnePow
+
+end Int

Mathlib/Algebra/Field/ZMod.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2018 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes
+-/
+import Mathlib.Algebra.Field.Basic
+import Mathlib.Data.ZMod.Basic
+
+/-!
+# `ZMod p` is a field
+-/
+
+namespace ZMod
+variable (p : ℕ) [hp : Fact p.Prime]
+
+private theorem mul_inv_cancel_aux (a : ZMod p) (h : a ≠ 0) : a * a⁻¹ = 1 := by
+  obtain ⟨k, rfl⟩ := natCast_zmod_surjective a
+  apply coe_mul_inv_eq_one
+  apply Nat.Coprime.symm
+  rwa [Nat.Prime.coprime_iff_not_dvd Fact.out, ← CharP.cast_eq_zero_iff (ZMod p)]
+
+/-- Field structure on `ZMod p` if `p` is prime. -/
+instance : Field (ZMod p) where
+  mul_inv_cancel := mul_inv_cancel_aux p
+  inv_zero := inv_zero p
+  nnqsmul := _
+  nnqsmul_def := fun _ _ => rfl
+  qsmul := _
+  qsmul_def := fun _ _ => rfl
+
+/-- `ZMod p` is an integral domain when `p` is prime. -/
+instance : IsDomain (ZMod p) := by
+  -- We need `cases p` here in order to resolve which `CommRing` instance is being used.
+  cases p
+  · exact (Nat.not_prime_zero hp.out).elim
+  exact @Field.isDomain (ZMod _) (inferInstanceAs (Field (ZMod _)))
+
+end ZMod

Mathlib/Algebra/Ring/NegOnePow.lean

@@ -6,7 +6,6 @@ Authors: Joël Riou, Johan Commelin
 import Mathlib.Algebra.Ring.Int.Parity
 import Mathlib.Algebra.Ring.Int.Units
 import Mathlib.Data.ZMod.IntUnitsPower
-import Mathlib.Tactic.NormNum
 
 /-!
 # Integer powers of (-1)
@@ -18,6 +17,7 @@ Johan Commelin to the Liquid Tensor Experiment.
 
 -/
 
+assert_not_exists Field
 assert_not_exists TwoSidedIdeal
 
 namespace Int
@@ -105,14 +105,6 @@ lemma negOnePow_eq_iff (n₁ n₂ : ℤ) :
 lemma negOnePow_mul_self (n : ℤ) : (n * n).negOnePow = n.negOnePow := by
   simpa [mul_sub, negOnePow_eq_iff] using n.even_mul_pred_self
 
-lemma cast_negOnePow (K : Type*) (n : ℤ) [Field K] : n.negOnePow = (-1 : K) ^ n := by
-  rcases even_or_odd' n with ⟨k, rfl | rfl⟩
-  · simp [zpow_mul, zpow_ofNat]
-  · rw [zpow_add_one₀ (by norm_num), zpow_mul, zpow_ofNat]
-    simp
-
-@[deprecated (since := "2024-10-20")] alias coe_negOnePow := cast_negOnePow
-
 lemma cast_negOnePow_natCast (R : Type*) [Ring R] (n : ℕ) : negOnePow n = (-1 : R) ^ n := by
   obtain ⟨k, rfl | rfl⟩ := Nat.even_or_odd' n <;> simp [pow_succ, pow_mul]
 

Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

@@ -3,9 +3,9 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin Davidson
 -/
+import Mathlib.Algebra.Field.NegOnePow
 import Mathlib.Algebra.Periodic
 import Mathlib.Algebra.QuadraticDiscriminant
-import Mathlib.Algebra.Ring.NegOnePow
 import Mathlib.Analysis.SpecialFunctions.Exp
 import Mathlib.Tactic.Positivity.Core
 

Mathlib/Data/ZMod/Basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
 import Mathlib.Algebra.CharP.Basic
-import Mathlib.Algebra.Field.Basic
 import Mathlib.Algebra.Module.End
 import Mathlib.Algebra.Ring.Prod
 import Mathlib.Data.Fintype.Units
@@ -31,7 +30,7 @@ This is a ring hom if the ring has characteristic dividing `n`
 
 -/
 
-assert_not_exists Submodule TwoSidedIdeal
+assert_not_exists Field Submodule TwoSidedIdeal
 
 open Function ZMod
 
@@ -1051,30 +1050,6 @@ theorem natAbs_min_of_le_div_two (n : ℕ) (x y : ℤ) (he : (x : ZMod n) = y) (
   refine le_trans ?_ (Nat.le_mul_of_pos_right _ <| Int.natAbs_pos.2 hm)
   rw [← mul_two]; apply Nat.div_mul_le_self
 
-variable (p : ℕ) [Fact p.Prime]
-
-private theorem mul_inv_cancel_aux (a : ZMod p) (h : a ≠ 0) : a * a⁻¹ = 1 := by
-  obtain ⟨k, rfl⟩ := natCast_zmod_surjective a
-  apply coe_mul_inv_eq_one
-  apply Nat.Coprime.symm
-  rwa [Nat.Prime.coprime_iff_not_dvd Fact.out, ← CharP.cast_eq_zero_iff (ZMod p)]
-
-/-- Field structure on `ZMod p` if `p` is prime. -/
-instance instField : Field (ZMod p) where
-  mul_inv_cancel := mul_inv_cancel_aux p
-  inv_zero := inv_zero p
-  nnqsmul := _
-  nnqsmul_def := fun _ _ => rfl
-  qsmul := _
-  qsmul_def := fun _ _ => rfl
-
-/-- `ZMod p` is an integral domain when `p` is prime. -/
-instance (p : ℕ) [hp : Fact p.Prime] : IsDomain (ZMod p) := by
-  -- We need `cases p` here in order to resolve which `CommRing` instance is being used.
-  cases p
-  · exact (Nat.not_prime_zero hp.out).elim
-  exact @Field.isDomain (ZMod _) (inferInstanceAs (Field (ZMod _)))
-
 end ZMod
 
 theorem RingHom.ext_zmod {n : ℕ} {R : Type*} [Semiring R] (f g : ZMod n →+* R) : f = g := by

Mathlib/FieldTheory/Finite/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Joey van Langen, Casper Putz
 -/
 import Mathlib.Algebra.CharP.Reduced
+import Mathlib.Algebra.Field.ZMod
 import Mathlib.Data.ZMod.ValMinAbs
 import Mathlib.FieldTheory.Separable
 import Mathlib.RingTheory.IntegralDomain

Mathlib/FieldTheory/IsAlgClosed/Classification.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
 import Mathlib.Algebra.Algebra.ZMod
+import Mathlib.Algebra.Field.ZMod
 import Mathlib.Algebra.MvPolynomial.Cardinal
 import Mathlib.Algebra.Polynomial.Cardinal
 import Mathlib.FieldTheory.IsAlgClosed.Basic

Mathlib/NumberTheory/LucasPrimality.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Bolton Bailey. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bolton Bailey
 -/
+import Mathlib.Algebra.Field.ZMod
 import Mathlib.RingTheory.IntegralDomain
 
 /-!

Mathlib/NumberTheory/Padics/RingHoms.lean

@@ -3,8 +3,9 @@ Copyright (c) 2020 Johan Commelin, Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Robert Y. Lewis
 -/
-import Mathlib.RingTheory.LocalRing.ResidueField.Defs
+import Mathlib.Algebra.Field.ZMod
 import Mathlib.NumberTheory.Padics.PadicIntegers
+import Mathlib.RingTheory.LocalRing.ResidueField.Defs
 import Mathlib.RingTheory.ZMod
 
 /-!

Mathlib/RingTheory/Polynomial/Dickson.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.CharP.Algebra
 import Mathlib.Algebra.CharP.Invertible
 import Mathlib.Algebra.CharP.Lemmas
 import Mathlib.Algebra.EuclideanDomain.Field
+import Mathlib.Algebra.Field.ZMod
 import Mathlib.Algebra.Polynomial.Roots
 import Mathlib.RingTheory.Polynomial.Chebyshev
 

MathlibTest/instance_diamonds.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.Algebra.EuclideanDomain.Field
+import Mathlib.Algebra.Field.ZMod
 import Mathlib.Algebra.GroupWithZero.Action.Prod
 import Mathlib.Algebra.GroupWithZero.Action.Units
 import Mathlib.Algebra.Module.Pi