diff --git a/Mathlib.lean b/Mathlib.lean
index 0c72da27c464b..ef847312a1d65 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -244,12 +244,15 @@ 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.Periodic
 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
@@ -849,7 +852,6 @@ import Mathlib.Algebra.Order.ToIntervalMod
 import Mathlib.Algebra.Order.UpperLower
 import Mathlib.Algebra.Order.ZeroLEOne
 import Mathlib.Algebra.PEmptyInstances
-import Mathlib.Algebra.Periodic
 import Mathlib.Algebra.Pointwise.Stabilizer
 import Mathlib.Algebra.Polynomial.AlgebraMap
 import Mathlib.Algebra.Polynomial.Basic
@@ -955,6 +957,7 @@ import Mathlib.Algebra.Ring.NonZeroDivisors
 import Mathlib.Algebra.Ring.Opposite
 import Mathlib.Algebra.Ring.PUnit
 import Mathlib.Algebra.Ring.Parity
+import Mathlib.Algebra.Ring.Periodic
 import Mathlib.Algebra.Ring.Pi
 import Mathlib.Algebra.Ring.Pointwise.Finset
 import Mathlib.Algebra.Ring.Pointwise.Set
diff --git a/Mathlib/Algebra/Field/NegOnePow.lean b/Mathlib/Algebra/Field/NegOnePow.lean
new file mode 100644
index 0000000000000..09830004cd053
--- /dev/null
+++ b/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
diff --git a/Mathlib/Algebra/Field/Periodic.lean b/Mathlib/Algebra/Field/Periodic.lean
new file mode 100644
index 0000000000000..73d41ddf2d66a
--- /dev/null
+++ b/Mathlib/Algebra/Field/Periodic.lean
@@ -0,0 +1,164 @@
+/-
+Copyright (c) 2021 Benjamin Davidson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Benjamin Davidson
+-/
+import Mathlib.Algebra.Field.Opposite
+import Mathlib.Algebra.Module.Opposite
+import Mathlib.Algebra.Order.Archimedean.Basic
+import Mathlib.Algebra.Ring.Periodic
+
+/-!
+# Periodic functions
+
+This file proves facts about periodic and antiperiodic functions from and to a field.
+
+## Main definitions
+
+* `Function.Periodic`: A function `f` is *periodic* if `∀ x, f (x + c) = f x`.
+  `f` is referred to as periodic with period `c` or `c`-periodic.
+
+* `Function.Antiperiodic`: A function `f` is *antiperiodic* if `∀ x, f (x + c) = -f x`.
+  `f` is referred to as antiperiodic with antiperiod `c` or `c`-antiperiodic.
+
+Note that any `c`-antiperiodic function will necessarily also be `2 • c`-periodic.
+
+## Tags
+
+period, periodic, periodicity, antiperiodic
+-/
+
+assert_not_exists TwoSidedIdeal
+
+variable {α β γ : Type*} {f g : α → β} {c c₁ c₂ x : α}
+
+open Set
+
+namespace Function
+
+/-! ### Periodicity -/
+
+protected theorem Periodic.const_smul₀ [AddCommMonoid α] [DivisionSemiring γ] [Module γ α]
+    (h : Periodic f c) (a : γ) : Periodic (fun x => f (a • x)) (a⁻¹ • c) := fun x => by
+  by_cases ha : a = 0
+  · simp only [ha, zero_smul]
+  · simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)
+
+protected theorem Periodic.const_mul [DivisionSemiring α] (h : Periodic f c) (a : α) :
+    Periodic (fun x => f (a * x)) (a⁻¹ * c) :=
+  Periodic.const_smul₀ h a
+
+theorem Periodic.const_inv_smul₀ [AddCommMonoid α] [DivisionSemiring γ] [Module γ α]
+    (h : Periodic f c) (a : γ) : Periodic (fun x => f (a⁻¹ • x)) (a • c) := by
+  simpa only [inv_inv] using h.const_smul₀ a⁻¹
+
+theorem Periodic.const_inv_mul [DivisionSemiring α] (h : Periodic f c) (a : α) :
+    Periodic (fun x => f (a⁻¹ * x)) (a * c) :=
+  h.const_inv_smul₀ a
+
+theorem Periodic.mul_const [DivisionSemiring α] (h : Periodic f c) (a : α) :
+    Periodic (fun x => f (x * a)) (c * a⁻¹) :=
+  h.const_smul₀ (MulOpposite.op a)
+
+theorem Periodic.mul_const' [DivisionSemiring α] (h : Periodic f c) (a : α) :
+    Periodic (fun x => f (x * a)) (c / a) := by simpa only [div_eq_mul_inv] using h.mul_const a
+
+theorem Periodic.mul_const_inv [DivisionSemiring α] (h : Periodic f c) (a : α) :
+    Periodic (fun x => f (x * a⁻¹)) (c * a) :=
+  h.const_inv_smul₀ (MulOpposite.op a)
+
+theorem Periodic.div_const [DivisionSemiring α] (h : Periodic f c) (a : α) :
+    Periodic (fun x => f (x / a)) (c * a) := by simpa only [div_eq_mul_inv] using h.mul_const_inv a
+
+/-- If a function `f` is `Periodic` with positive period `c`, then for all `x` there exists some
+  `y ∈ Ico 0 c` such that `f x = f y`. -/
+theorem Periodic.exists_mem_Ico₀ [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
+    (hc : 0 < c) (x) : ∃ y ∈ Ico 0 c, f x = f y :=
+  let ⟨n, H, _⟩ := existsUnique_zsmul_near_of_pos' hc x
+  ⟨x - n • c, H, (h.sub_zsmul_eq n).symm⟩
+
+/-- If a function `f` is `Periodic` with positive period `c`, then for all `x` there exists some
+  `y ∈ Ico a (a + c)` such that `f x = f y`. -/
+theorem Periodic.exists_mem_Ico [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
+    (hc : 0 < c) (x a) : ∃ y ∈ Ico a (a + c), f x = f y :=
+  let ⟨n, H, _⟩ := existsUnique_add_zsmul_mem_Ico hc x a
+  ⟨x + n • c, H, (h.zsmul n x).symm⟩
+
+/-- If a function `f` is `Periodic` with positive period `c`, then for all `x` there exists some
+  `y ∈ Ioc a (a + c)` such that `f x = f y`. -/
+theorem Periodic.exists_mem_Ioc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
+    (hc : 0 < c) (x a) : ∃ y ∈ Ioc a (a + c), f x = f y :=
+  let ⟨n, H, _⟩ := existsUnique_add_zsmul_mem_Ioc hc x a
+  ⟨x + n • c, H, (h.zsmul n x).symm⟩
+
+theorem Periodic.image_Ioc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
+    (hc : 0 < c) (a : α) : f '' Ioc a (a + c) = range f :=
+  (image_subset_range _ _).antisymm <| range_subset_iff.2 fun x =>
+    let ⟨y, hy, hyx⟩ := h.exists_mem_Ioc hc x a
+    ⟨y, hy, hyx.symm⟩
+
+theorem Periodic.image_Icc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
+    (hc : 0 < c) (a : α) : f '' Icc a (a + c) = range f :=
+  (image_subset_range _ _).antisymm <| h.image_Ioc hc a ▸ image_subset _ Ioc_subset_Icc_self
+
+theorem Periodic.image_uIcc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
+    (hc : c ≠ 0) (a : α) : f '' uIcc a (a + c) = range f := by
+  cases hc.lt_or_lt with
+  | inl hc =>
+    rw [uIcc_of_ge (add_le_of_nonpos_right hc.le), ← h.neg.image_Icc (neg_pos.2 hc) (a + c),
+      add_neg_cancel_right]
+  | inr hc => rw [uIcc_of_le (le_add_of_nonneg_right hc.le), h.image_Icc hc]
+
+/-! ### Antiperiodicity -/
+
+theorem Antiperiodic.add_nat_mul_eq [Semiring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) :
+    f (x + n * c) = (-1) ^ n * f x := by
+  simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
+    Int.cast_one] using h.add_nsmul_eq n
+
+theorem Antiperiodic.sub_nat_mul_eq [Ring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) :
+    f (x - n * c) = (-1) ^ n * f x := by
+  simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
+    Int.cast_one] using h.sub_nsmul_eq n
+
+theorem Antiperiodic.nat_mul_sub_eq [Ring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) :
+    f (n * c - x) = (-1) ^ n * f (-x) := by
+  simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
+    Int.cast_one] using h.nsmul_sub_eq n
+
+theorem Antiperiodic.const_smul₀ [AddCommMonoid α] [Neg β] [DivisionSemiring γ] [Module γ α]
+    (h : Antiperiodic f c) {a : γ} (ha : a ≠ 0) : Antiperiodic (fun x => f (a • x)) (a⁻¹ • c) :=
+  fun x => by simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)
+
+theorem Antiperiodic.const_mul [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
+    (ha : a ≠ 0) : Antiperiodic (fun x => f (a * x)) (a⁻¹ * c) :=
+  h.const_smul₀ ha
+
+theorem Antiperiodic.const_inv_smul₀ [AddCommMonoid α] [Neg β] [DivisionSemiring γ] [Module γ α]
+    (h : Antiperiodic f c) {a : γ} (ha : a ≠ 0) : Antiperiodic (fun x => f (a⁻¹ • x)) (a • c) := by
+  simpa only [inv_inv] using h.const_smul₀ (inv_ne_zero ha)
+
+theorem Antiperiodic.const_inv_mul [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
+    (ha : a ≠ 0) : Antiperiodic (fun x => f (a⁻¹ * x)) (a * c) :=
+  h.const_inv_smul₀ ha
+
+theorem Antiperiodic.mul_const [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
+    (ha : a ≠ 0) : Antiperiodic (fun x => f (x * a)) (c * a⁻¹) :=
+  h.const_smul₀ <| (MulOpposite.op_ne_zero_iff a).mpr ha
+
+theorem Antiperiodic.mul_const' [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
+    (ha : a ≠ 0) : Antiperiodic (fun x => f (x * a)) (c / a) := by
+  simpa only [div_eq_mul_inv] using h.mul_const ha
+
+theorem Antiperiodic.mul_const_inv [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
+    (ha : a ≠ 0) : Antiperiodic (fun x => f (x * a⁻¹)) (c * a) :=
+  h.const_inv_smul₀ <| (MulOpposite.op_ne_zero_iff a).mpr ha
+
+theorem Antiperiodic.div_inv [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
+    (ha : a ≠ 0) : Antiperiodic (fun x => f (x / a)) (c * a) := by
+  simpa only [div_eq_mul_inv] using h.mul_const_inv ha
+
+end Function
+
+theorem Int.fract_periodic (α) [LinearOrderedRing α] [FloorRing α] :
+    Function.Periodic Int.fract (1 : α) := fun a => mod_cast Int.fract_add_int a 1
diff --git a/Mathlib/Algebra/Field/ZMod.lean b/Mathlib/Algebra/Field/ZMod.lean
new file mode 100644
index 0000000000000..7b0a67667b68b
--- /dev/null
+++ b/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
diff --git a/Mathlib/Algebra/Homology/ComplexShapeSigns.lean b/Mathlib/Algebra/Homology/ComplexShapeSigns.lean
index d4728724fe0c1..4600210c504df 100644
--- a/Mathlib/Algebra/Homology/ComplexShapeSigns.lean
+++ b/Mathlib/Algebra/Homology/ComplexShapeSigns.lean
@@ -24,7 +24,7 @@ satisfying certain properties (see `ComplexShape.TensorSigns`).
 
 -/
 
-assert_not_exists TwoSidedIdeal
+assert_not_exists Field TwoSidedIdeal
 
 variable {I₁ I₂ I₃ I₁₂ I₂₃ J : Type*}
   (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₃ : ComplexShape I₃)
diff --git a/Mathlib/Algebra/Order/ToIntervalMod.lean b/Mathlib/Algebra/Order/ToIntervalMod.lean
index a3b326dc85ff6..b5b77ce5af7a4 100644
--- a/Mathlib/Algebra/Order/ToIntervalMod.lean
+++ b/Mathlib/Algebra/Order/ToIntervalMod.lean
@@ -4,13 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
 -/
 import Mathlib.Algebra.ModEq
-import Mathlib.Algebra.Module.Defs
 import Mathlib.Algebra.Order.Archimedean.Basic
-import Mathlib.Algebra.Periodic
+import Mathlib.Algebra.Ring.Periodic
 import Mathlib.Data.Int.SuccPred
 import Mathlib.Order.Circular
-import Mathlib.Data.List.TFAE
-import Mathlib.Data.Set.Lattice
 
 /-!
 # Reducing to an interval modulo its length
diff --git a/Mathlib/Algebra/Ring/NegOnePow.lean b/Mathlib/Algebra/Ring/NegOnePow.lean
index 62d61d99068ed..194d23e68cc1a 100644
--- a/Mathlib/Algebra/Ring/NegOnePow.lean
+++ b/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]
 
diff --git a/Mathlib/Algebra/Periodic.lean b/Mathlib/Algebra/Ring/Periodic.lean
similarity index 71%
rename from Mathlib/Algebra/Periodic.lean
rename to Mathlib/Algebra/Ring/Periodic.lean
index 621cca880bcbd..52e43f7dd231e 100644
--- a/Mathlib/Algebra/Periodic.lean
+++ b/Mathlib/Algebra/Ring/Periodic.lean
@@ -3,13 +3,7 @@ Copyright (c) 2021 Benjamin Davidson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Benjamin Davidson
 -/
-import Mathlib.Algebra.Field.Opposite
-import Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
-import Mathlib.Algebra.Group.Submonoid.Membership
-import Mathlib.Algebra.Module.Opposite
-import Mathlib.Algebra.Order.Archimedean.Basic
 import Mathlib.Algebra.Ring.NegOnePow
-import Mathlib.GroupTheory.Coset.Card
 
 /-!
 # Periodicity
@@ -31,7 +25,7 @@ Note that any `c`-antiperiodic function will necessarily also be `2 • c`-perio
 period, periodic, periodicity, antiperiodic
 -/
 
-assert_not_exists TwoSidedIdeal
+assert_not_exists Field
 
 variable {α β γ : Type*} {f g : α → β} {c c₁ c₂ x : α}
 
@@ -92,42 +86,10 @@ protected theorem Periodic.const_smul [AddMonoid α] [Group γ] [DistribMulActio
     (h : Periodic f c) (a : γ) : Periodic (fun x => f (a • x)) (a⁻¹ • c) := fun x => by
   simpa only [smul_add, smul_inv_smul] using h (a • x)
 
-protected theorem Periodic.const_smul₀ [AddCommMonoid α] [DivisionSemiring γ] [Module γ α]
-    (h : Periodic f c) (a : γ) : Periodic (fun x => f (a • x)) (a⁻¹ • c) := fun x => by
-  by_cases ha : a = 0
-  · simp only [ha, zero_smul]
-  · simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)
-
-protected theorem Periodic.const_mul [DivisionSemiring α] (h : Periodic f c) (a : α) :
-    Periodic (fun x => f (a * x)) (a⁻¹ * c) :=
-  Periodic.const_smul₀ h a
-
 theorem Periodic.const_inv_smul [AddMonoid α] [Group γ] [DistribMulAction γ α] (h : Periodic f c)
     (a : γ) : Periodic (fun x => f (a⁻¹ • x)) (a • c) := by
   simpa only [inv_inv] using h.const_smul a⁻¹
 
-theorem Periodic.const_inv_smul₀ [AddCommMonoid α] [DivisionSemiring γ] [Module γ α]
-    (h : Periodic f c) (a : γ) : Periodic (fun x => f (a⁻¹ • x)) (a • c) := by
-  simpa only [inv_inv] using h.const_smul₀ a⁻¹
-
-theorem Periodic.const_inv_mul [DivisionSemiring α] (h : Periodic f c) (a : α) :
-    Periodic (fun x => f (a⁻¹ * x)) (a * c) :=
-  h.const_inv_smul₀ a
-
-theorem Periodic.mul_const [DivisionSemiring α] (h : Periodic f c) (a : α) :
-    Periodic (fun x => f (x * a)) (c * a⁻¹) :=
-  h.const_smul₀ (MulOpposite.op a)
-
-theorem Periodic.mul_const' [DivisionSemiring α] (h : Periodic f c) (a : α) :
-    Periodic (fun x => f (x * a)) (c / a) := by simpa only [div_eq_mul_inv] using h.mul_const a
-
-theorem Periodic.mul_const_inv [DivisionSemiring α] (h : Periodic f c) (a : α) :
-    Periodic (fun x => f (x * a⁻¹)) (c * a) :=
-  h.const_inv_smul₀ (MulOpposite.op a)
-
-theorem Periodic.div_const [DivisionSemiring α] (h : Periodic f c) (a : α) :
-    Periodic (fun x => f (x / a)) (c * a) := by simpa only [div_eq_mul_inv] using h.mul_const_inv a
-
 theorem Periodic.add_period [AddSemigroup α] (h1 : Periodic f c₁) (h2 : Periodic f c₂) :
     Periodic f (c₁ + c₂) := by simp_all [← add_assoc]
 
@@ -223,45 +185,6 @@ theorem Periodic.zsmul_eq [AddGroup α] (h : Periodic f c) (n : ℤ) : f (n •
 theorem Periodic.int_mul_eq [Ring α] (h : Periodic f c) (n : ℤ) : f (n * c) = f 0 :=
   (h.int_mul n).eq
 
-/-- If a function `f` is `Periodic` with positive period `c`, then for all `x` there exists some
-  `y ∈ Ico 0 c` such that `f x = f y`. -/
-theorem Periodic.exists_mem_Ico₀ [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
-    (hc : 0 < c) (x) : ∃ y ∈ Ico 0 c, f x = f y :=
-  let ⟨n, H, _⟩ := existsUnique_zsmul_near_of_pos' hc x
-  ⟨x - n • c, H, (h.sub_zsmul_eq n).symm⟩
-
-/-- If a function `f` is `Periodic` with positive period `c`, then for all `x` there exists some
-  `y ∈ Ico a (a + c)` such that `f x = f y`. -/
-theorem Periodic.exists_mem_Ico [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
-    (hc : 0 < c) (x a) : ∃ y ∈ Ico a (a + c), f x = f y :=
-  let ⟨n, H, _⟩ := existsUnique_add_zsmul_mem_Ico hc x a
-  ⟨x + n • c, H, (h.zsmul n x).symm⟩
-
-/-- If a function `f` is `Periodic` with positive period `c`, then for all `x` there exists some
-  `y ∈ Ioc a (a + c)` such that `f x = f y`. -/
-theorem Periodic.exists_mem_Ioc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
-    (hc : 0 < c) (x a) : ∃ y ∈ Ioc a (a + c), f x = f y :=
-  let ⟨n, H, _⟩ := existsUnique_add_zsmul_mem_Ioc hc x a
-  ⟨x + n • c, H, (h.zsmul n x).symm⟩
-
-theorem Periodic.image_Ioc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
-    (hc : 0 < c) (a : α) : f '' Ioc a (a + c) = range f :=
-  (image_subset_range _ _).antisymm <| range_subset_iff.2 fun x =>
-    let ⟨y, hy, hyx⟩ := h.exists_mem_Ioc hc x a
-    ⟨y, hy, hyx.symm⟩
-
-theorem Periodic.image_Icc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
-    (hc : 0 < c) (a : α) : f '' Icc a (a + c) = range f :=
-  (image_subset_range _ _).antisymm <| h.image_Ioc hc a ▸ image_subset _ Ioc_subset_Icc_self
-
-theorem Periodic.image_uIcc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
-    (hc : c ≠ 0) (a : α) : f '' uIcc a (a + c) = range f := by
-  cases hc.lt_or_lt with
-  | inl hc =>
-    rw [uIcc_of_ge (add_le_of_nonpos_right hc.le), ← h.neg.image_Icc (neg_pos.2 hc) (a + c),
-      add_neg_cancel_right]
-  | inr hc => rw [uIcc_of_le (le_add_of_nonneg_right hc.le), h.image_Icc hc]
-
 theorem periodic_with_period_zero [AddZeroClass α] (f : α → β) : Periodic f 0 := fun x => by
   rw [add_zero]
 
@@ -406,9 +329,10 @@ theorem Antiperiodic.int_mul_sub_eq [Ring α] [Ring β] (h : Antiperiodic f c) (
 theorem Antiperiodic.add_nsmul_eq [AddMonoid α] [AddGroup β] (h : Antiperiodic f c) (n : ℕ) :
     f (x + n • c) = (-1) ^ n • f x := by
   rcases Nat.even_or_odd' n with ⟨k, rfl | rfl⟩
-  · rw [h.even_nsmul_periodic, pow_mul, (by norm_num : (-1) ^ 2 = 1), one_pow, one_zsmul]
-  · rw [h.odd_nsmul_antiperiodic, pow_add, pow_mul, (by norm_num : (-1) ^ 2 = 1), one_pow,
-      pow_one, one_mul, neg_zsmul, one_zsmul]
+  · rw [h.even_nsmul_periodic]
+    simp
+  · rw [h.odd_nsmul_antiperiodic]
+    simp [pow_add]
 
 theorem Antiperiodic.sub_nsmul_eq [AddGroup α] [AddGroup β] (h : Antiperiodic f c) (n : ℕ) :
     f (x - n • c) = (-1) ^ n • f x := by
@@ -418,21 +342,6 @@ theorem Antiperiodic.nsmul_sub_eq [AddCommGroup α] [AddGroup β] (h : Antiperio
     f (n • c - x) = (-1) ^ n • f (-x) := by
   simpa only [Int.reduceNeg, natCast_zsmul] using h.zsmul_sub_eq n
 
-theorem Antiperiodic.add_nat_mul_eq [Semiring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) :
-    f (x + n * c) = (-1) ^ n * f x := by
-  simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
-    Int.cast_one] using h.add_nsmul_eq n
-
-theorem Antiperiodic.sub_nat_mul_eq [Ring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) :
-    f (x - n * c) = (-1) ^ n * f x := by
-  simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
-    Int.cast_one] using h.sub_nsmul_eq n
-
-theorem Antiperiodic.nat_mul_sub_eq [Ring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) :
-    f (n * c - x) = (-1) ^ n * f (-x) := by
-  simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
-    Int.cast_one] using h.nsmul_sub_eq n
-
 theorem Antiperiodic.const_add [AddSemigroup α] [Neg β] (h : Antiperiodic f c) (a : α) :
     Antiperiodic (fun x => f (a + x)) c := fun x => by simpa [add_assoc] using h (a + x)
 
@@ -455,42 +364,10 @@ theorem Antiperiodic.const_smul [AddMonoid α] [Neg β] [Group γ] [DistribMulAc
     (h : Antiperiodic f c) (a : γ) : Antiperiodic (fun x => f (a • x)) (a⁻¹ • c) := fun x => by
   simpa only [smul_add, smul_inv_smul] using h (a • x)
 
-theorem Antiperiodic.const_smul₀ [AddCommMonoid α] [Neg β] [DivisionSemiring γ] [Module γ α]
-    (h : Antiperiodic f c) {a : γ} (ha : a ≠ 0) : Antiperiodic (fun x => f (a • x)) (a⁻¹ • c) :=
-  fun x => by simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)
-
-theorem Antiperiodic.const_mul [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
-    (ha : a ≠ 0) : Antiperiodic (fun x => f (a * x)) (a⁻¹ * c) :=
-  h.const_smul₀ ha
-
 theorem Antiperiodic.const_inv_smul [AddMonoid α] [Neg β] [Group γ] [DistribMulAction γ α]
     (h : Antiperiodic f c) (a : γ) : Antiperiodic (fun x => f (a⁻¹ • x)) (a • c) := by
   simpa only [inv_inv] using h.const_smul a⁻¹
 
-theorem Antiperiodic.const_inv_smul₀ [AddCommMonoid α] [Neg β] [DivisionSemiring γ] [Module γ α]
-    (h : Antiperiodic f c) {a : γ} (ha : a ≠ 0) : Antiperiodic (fun x => f (a⁻¹ • x)) (a • c) := by
-  simpa only [inv_inv] using h.const_smul₀ (inv_ne_zero ha)
-
-theorem Antiperiodic.const_inv_mul [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
-    (ha : a ≠ 0) : Antiperiodic (fun x => f (a⁻¹ * x)) (a * c) :=
-  h.const_inv_smul₀ ha
-
-theorem Antiperiodic.mul_const [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
-    (ha : a ≠ 0) : Antiperiodic (fun x => f (x * a)) (c * a⁻¹) :=
-  h.const_smul₀ <| (MulOpposite.op_ne_zero_iff a).mpr ha
-
-theorem Antiperiodic.mul_const' [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
-    (ha : a ≠ 0) : Antiperiodic (fun x => f (x * a)) (c / a) := by
-  simpa only [div_eq_mul_inv] using h.mul_const ha
-
-theorem Antiperiodic.mul_const_inv [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
-    (ha : a ≠ 0) : Antiperiodic (fun x => f (x * a⁻¹)) (c * a) :=
-  h.const_inv_smul₀ <| (MulOpposite.op_ne_zero_iff a).mpr ha
-
-theorem Antiperiodic.div_inv [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
-    (ha : a ≠ 0) : Antiperiodic (fun x => f (x / a)) (c * a) := by
-  simpa only [div_eq_mul_inv] using h.mul_const_inv ha
-
 theorem Antiperiodic.add [AddGroup α] [InvolutiveNeg β] (h1 : Antiperiodic f c₁)
     (h2 : Antiperiodic f c₂) : Periodic f (c₁ + c₂) := by simp_all [← add_assoc]
 
@@ -520,6 +397,3 @@ theorem Antiperiodic.div [Add α] [DivisionMonoid β] [HasDistribNeg β] (hf : A
     (hg : Antiperiodic g c) : Periodic (f / g) c := by simp_all [neg_div_neg_eq]
 
 end Function
-
-theorem Int.fract_periodic (α) [LinearOrderedRing α] [FloorRing α] :
-    Function.Periodic Int.fract (1 : α) := fun a => mod_cast Int.fract_add_int a 1
diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
index e2816cc24eaff..ae6124358c8ee 100644
--- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
@@ -3,11 +3,10 @@ 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.Periodic
+import Mathlib.Algebra.Field.NegOnePow
+import Mathlib.Algebra.Field.Periodic
 import Mathlib.Algebra.QuadraticDiscriminant
-import Mathlib.Algebra.Ring.NegOnePow
 import Mathlib.Analysis.SpecialFunctions.Exp
-import Mathlib.Tactic.Positivity.Core
 
 /-!
 # Trigonometric functions
diff --git a/Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean b/Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
index 4cec4e8b8fee7..d2d42a3b42cff 100644
--- a/Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
@@ -35,7 +35,7 @@ of the corresponding vertex and that (2) the map from darts to edges is 2-to-1.
 simple graphs, sums, degree-sum formula, handshaking lemma
 -/
 
-assert_not_exists TwoSidedIdeal
+assert_not_exists Field TwoSidedIdeal
 
 open Finset
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Matching.lean b/Mathlib/Combinatorics/SimpleGraph/Matching.lean
index 310d9aa562bd1..2e949566408f9 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Matching.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Matching.lean
@@ -46,7 +46,7 @@ one edge, and the edges of the subgraph represent the paired vertices.
 * Hall's Marriage Theorem (see `Mathlib.Combinatorics.Hall.Basic`)
 -/
 
-assert_not_exists TwoSidedIdeal
+assert_not_exists Field TwoSidedIdeal
 
 open Function
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/UniversalVerts.lean b/Mathlib/Combinatorics/SimpleGraph/UniversalVerts.lean
index a144fe4148ce7..9aeb6dbccfb6b 100644
--- a/Mathlib/Combinatorics/SimpleGraph/UniversalVerts.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/UniversalVerts.lean
@@ -20,7 +20,7 @@ in the proof of Tutte's Theorem.
 * `G.deleteUniversalVerts` is the subgraph of `G` with the universal vertices removed.
 -/
 
-assert_not_exists TwoSidedIdeal
+assert_not_exists Field TwoSidedIdeal
 
 namespace SimpleGraph
 variable {V : Type*} {G : SimpleGraph V}
diff --git a/Mathlib/Data/Nat/Periodic.lean b/Mathlib/Data/Nat/Periodic.lean
index d1128353419d6..d86a28f1af4a8 100644
--- a/Mathlib/Data/Nat/Periodic.lean
+++ b/Mathlib/Data/Nat/Periodic.lean
@@ -3,10 +3,8 @@ Copyright (c) 2021 Bolton Bailey. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bolton Bailey
 -/
-import Mathlib.Algebra.Periodic
+import Mathlib.Algebra.Ring.Periodic
 import Mathlib.Data.Nat.Count
-import Mathlib.Data.Nat.GCD.Basic
-import Mathlib.Order.Interval.Finset.Nat
 
 /-!
 # Periodic Functions on ℕ
diff --git a/Mathlib/Data/Nat/Totient.lean b/Mathlib/Data/Nat/Totient.lean
index 41552a50cc4d4..e1e97c358f682 100644
--- a/Mathlib/Data/Nat/Totient.lean
+++ b/Mathlib/Data/Nat/Totient.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
 import Mathlib.Algebra.CharP.Two
+import Mathlib.Algebra.CharZero.Lemmas
 import Mathlib.Data.Nat.Factorization.Basic
 import Mathlib.Data.Nat.Factorization.Induction
 import Mathlib.Data.Nat.Periodic
diff --git a/Mathlib/Data/ZMod/Aut.lean b/Mathlib/Data/ZMod/Aut.lean
index 7b553f70fa2fd..13d5333aa183c 100644
--- a/Mathlib/Data/ZMod/Aut.lean
+++ b/Mathlib/Data/ZMod/Aut.lean
@@ -10,7 +10,7 @@ import Mathlib.Data.ZMod.Basic
 # Automorphism Group of `ZMod`.
 -/
 
-assert_not_exists TwoSidedIdeal
+assert_not_exists Field TwoSidedIdeal
 
 namespace ZMod
 
diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean
index 59afdd1965ae0..890c9d1e9851f 100644
--- a/Mathlib/Data/ZMod/Basic.lean
+++ b/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
diff --git a/Mathlib/FieldTheory/Finite/Basic.lean b/Mathlib/FieldTheory/Finite/Basic.lean
index 4a4520e252613..470736132fec3 100644
--- a/Mathlib/FieldTheory/Finite/Basic.lean
+++ b/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
diff --git a/Mathlib/FieldTheory/IsAlgClosed/Classification.lean b/Mathlib/FieldTheory/IsAlgClosed/Classification.lean
index 4ca1dd6b4fbde..10480781dff2a 100644
--- a/Mathlib/FieldTheory/IsAlgClosed/Classification.lean
+++ b/Mathlib/FieldTheory/IsAlgClosed/Classification.lean
@@ -4,8 +4,8 @@ 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
 import Mathlib.RingTheory.Algebraic.Cardinality
 import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
diff --git a/Mathlib/GroupTheory/Perm/Centralizer.lean b/Mathlib/GroupTheory/Perm/Centralizer.lean
index d347a5a378fb5..b5e1f0cba1739 100644
--- a/Mathlib/GroupTheory/Perm/Centralizer.lean
+++ b/Mathlib/GroupTheory/Perm/Centralizer.lean
@@ -3,17 +3,13 @@ Copyright (c) 2023 Antoine Chambert-Loir. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Chambert-Loir
 -/
-
 import Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
 import Mathlib.Algebra.Order.BigOperators.Ring.Finset
 import Mathlib.GroupTheory.Finiteness
 import Mathlib.GroupTheory.NoncommCoprod
-import Mathlib.GroupTheory.NoncommPiCoprod
 import Mathlib.GroupTheory.Perm.ConjAct
-import Mathlib.GroupTheory.Perm.Cycle.Factors
 import Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
 import Mathlib.GroupTheory.Perm.DomMulAct
-import Mathlib.GroupTheory.Perm.Finite
 
 /-! # Centralizer of a permutation and cardinality of conjugacy classes
   # in the symmetric groups
diff --git a/Mathlib/GroupTheory/Sylow.lean b/Mathlib/GroupTheory/Sylow.lean
index 7c7d7efa40cf2..bd1f73fe17cfa 100644
--- a/Mathlib/GroupTheory/Sylow.lean
+++ b/Mathlib/GroupTheory/Sylow.lean
@@ -3,6 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Thomas Browning
 -/
+import Mathlib.Algebra.Order.Archimedean.Basic
 import Mathlib.Data.SetLike.Fintype
 import Mathlib.GroupTheory.PGroup
 import Mathlib.GroupTheory.NoncommPiCoprod
diff --git a/Mathlib/NumberTheory/FermatPsp.lean b/Mathlib/NumberTheory/FermatPsp.lean
index 5c593d0213ec5..57a71cba47924 100644
--- a/Mathlib/NumberTheory/FermatPsp.lean
+++ b/Mathlib/NumberTheory/FermatPsp.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Niels Voss. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Niels Voss
 -/
+import Mathlib.Algebra.Order.Archimedean.Basic
 import Mathlib.FieldTheory.Finite.Basic
 import Mathlib.Order.Filter.Cofinite
 
diff --git a/Mathlib/NumberTheory/LucasPrimality.lean b/Mathlib/NumberTheory/LucasPrimality.lean
index 34deef6e5fc10..39e0f93a7b61b 100644
--- a/Mathlib/NumberTheory/LucasPrimality.lean
+++ b/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
 
 /-!
diff --git a/Mathlib/NumberTheory/Padics/RingHoms.lean b/Mathlib/NumberTheory/Padics/RingHoms.lean
index a4bc7e4bf2fd8..bb16e4b29ac1e 100644
--- a/Mathlib/NumberTheory/Padics/RingHoms.lean
+++ b/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
 
 /-!
diff --git a/Mathlib/RingTheory/IntegralDomain.lean b/Mathlib/RingTheory/IntegralDomain.lean
index 57d9cf6e6bfb4..ad695d0a3b0bb 100644
--- a/Mathlib/RingTheory/IntegralDomain.lean
+++ b/Mathlib/RingTheory/IntegralDomain.lean
@@ -6,6 +6,7 @@ Authors: Johan Commelin, Chris Hughes
 import Mathlib.Algebra.GeomSum
 import Mathlib.Algebra.Polynomial.Roots
 import Mathlib.GroupTheory.SpecificGroups.Cyclic
+import Mathlib.Tactic.FieldSimp
 
 /-!
 # Integral domains
diff --git a/Mathlib/RingTheory/Polynomial/Dickson.lean b/Mathlib/RingTheory/Polynomial/Dickson.lean
index d1a85a4548180..aee0c850d5b64 100644
--- a/Mathlib/RingTheory/Polynomial/Dickson.lean
+++ b/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
 
diff --git a/Mathlib/Topology/ContinuousMap/Periodic.lean b/Mathlib/Topology/ContinuousMap/Periodic.lean
index c841c62c108a0..bada29d8073fd 100644
--- a/Mathlib/Topology/ContinuousMap/Periodic.lean
+++ b/Mathlib/Topology/ContinuousMap/Periodic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison, Nicolò Cavalleri
 -/
-import Mathlib.Algebra.Periodic
+import Mathlib.Algebra.Ring.Periodic
 import Mathlib.Topology.ContinuousMap.Algebra
 
 /-!
diff --git a/Mathlib/Topology/Instances/Real/Lemmas.lean b/Mathlib/Topology/Instances/Real/Lemmas.lean
index 3ba8704780b0b..833b1eb785fe9 100644
--- a/Mathlib/Topology/Instances/Real/Lemmas.lean
+++ b/Mathlib/Topology/Instances/Real/Lemmas.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
-import Mathlib.Algebra.Periodic
+import Mathlib.Algebra.Field.Periodic
 import Mathlib.Topology.Algebra.Order.Archimedean
 import Mathlib.Topology.Instances.Real.Defs
 
diff --git a/Mathlib/Topology/Instances/ZMultiples.lean b/Mathlib/Topology/Instances/ZMultiples.lean
index 11fa9965bd443..a3a72935e3632 100644
--- a/Mathlib/Topology/Instances/ZMultiples.lean
+++ b/Mathlib/Topology/Instances/ZMultiples.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Algebra.Algebra.Rat
+import Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
 import Mathlib.Algebra.Module.Rat
 import Mathlib.Algebra.Module.Submodule.Lattice
 import Mathlib.Topology.Algebra.UniformGroup.Basic
diff --git a/MathlibTest/instance_diamonds.lean b/MathlibTest/instance_diamonds.lean
index 02932d2f6192b..1dffa9c372c1c 100644
--- a/MathlibTest/instance_diamonds.lean
+++ b/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