chore: reduce imports in ZMod.Basic (#12478)

- While at it, document the lemmas that were moved, and two similar lemmas in `ZMod.Basic`.



Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>

Mathlib/Data/ZMod/Basic.lean

@@ -4,9 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
 import Mathlib.Algebra.CharP.Basic
-import Mathlib.RingTheory.Ideal.Operations
-import Mathlib.Data.Fintype.Units
-import Mathlib.Data.Nat.Parity
+import Mathlib.Algebra.Ring.Prod
 import Mathlib.Tactic.FinCases
 
 #align_import data.zmod.basic from "leanprover-community/mathlib"@"74ad1c88c77e799d2fea62801d1dbbd698cff1b7"
@@ -32,6 +30,8 @@ This is a ring hom if the ring has characteristic dividing `n`
 
 -/
 
+assert_not_exists Submodule
+
 open Function
 
 namespace ZMod
@@ -599,12 +599,6 @@ theorem ker_intCastAddHom (n : ℕ) :
     intCast_zmod_eq_zero_iff_dvd]
 #align zmod.ker_int_cast_add_hom ZMod.ker_intCastAddHom
 
-theorem ker_intCastRingHom (n : ℕ) :
-    RingHom.ker (Int.castRingHom (ZMod n)) = Ideal.span ({(n : ℤ)} : Set ℤ) := by
-  ext
-  rw [Ideal.mem_span_singleton, RingHom.mem_ker, Int.coe_castRingHom, intCast_zmod_eq_zero_iff_dvd]
-#align zmod.ker_int_cast_ring_hom ZMod.ker_intCastRingHom
-
 theorem cast_injective_of_le {m n : ℕ} [nzm : NeZero m] (h : m ≤ n) :
     Function.Injective (@cast (ZMod n) _ m) := by
   cases m with
@@ -1292,22 +1286,17 @@ theorem ringHom_map_cast [Ring R] (f : R →+* ZMod n) (k : ZMod n) : f (cast k)
     erw [map_natCast, Fin.cast_val_eq_self]
 #align zmod.ring_hom_map_cast ZMod.ringHom_map_cast
 
+/-- Any ring homomorphism into `ZMod n` has a right inverse. -/
 theorem ringHom_rightInverse [Ring R] (f : R →+* ZMod n) :
     Function.RightInverse (cast : ZMod n → R) f :=
   ringHom_map_cast f
 #align zmod.ring_hom_right_inverse ZMod.ringHom_rightInverse
 
+/-- Any ring homomorphism into `ZMod n` is surjective. -/
 theorem ringHom_surjective [Ring R] (f : R →+* ZMod n) : Function.Surjective f :=
   (ringHom_rightInverse f).surjective
 #align zmod.ring_hom_surjective ZMod.ringHom_surjective
 
-theorem ringHom_eq_of_ker_eq [CommRing R] (f g : R →+* ZMod n)
-    (h : RingHom.ker f = RingHom.ker g) : f = g := by
-  have := f.liftOfRightInverse_comp _ (ZMod.ringHom_rightInverse f) ⟨g, le_of_eq h⟩
-  rw [Subtype.coe_mk] at this
-  rw [← this, RingHom.ext_zmod (f.liftOfRightInverse _ _ ⟨g, _⟩) _, RingHom.id_comp]
-#align zmod.ring_hom_eq_of_ker_eq ZMod.ringHom_eq_of_ker_eq
-
 @[simp]
 lemma castHom_self : ZMod.castHom dvd_rfl (ZMod n) = RingHom.id (ZMod n) :=
   Subsingleton.elim _ _

Mathlib/Data/ZMod/Module.lean

@@ -3,8 +3,9 @@ Copyright (c) 2023 Lawrence Wu. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lawrence Wu
 -/
+import Mathlib.Algebra.Module.Submodule.Lattice
 import Mathlib.Data.ZMod.Basic
-import Mathlib.Algebra.Module.LinearMap.Basic
+import Mathlib.Order.OmegaCompletePartialOrder
 
 /-!
 # The `ZMod n`-module structure on Abelian groups whose elements have order dividing `n`

Mathlib/Data/ZMod/Quotient.lean

@@ -8,6 +8,7 @@ import Mathlib.Data.ZMod.Basic
 import Mathlib.GroupTheory.GroupAction.Quotient
 import Mathlib.RingTheory.Ideal.QuotientOperations
 import Mathlib.RingTheory.Int.Basic
+import Mathlib.RingTheory.ZMod
 
 #align_import data.zmod.quotient from "leanprover-community/mathlib"@"da420a8c6dd5bdfb85c4ced85c34388f633bc6ff"
 

Mathlib/Data/ZMod/Units.lean

@@ -3,10 +3,10 @@ Copyright (c) 2023 Moritz Firsching. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Moritz Firsching, Ashvni Narayanan, Michael Stoll
 -/
+import Mathlib.Algebra.BigOperators.Associated
 import Mathlib.Data.ZMod.Basic
 import Mathlib.Data.Nat.PrimeFin
-import Mathlib.Algebra.BigOperators.Associated
-
+import Mathlib.RingTheory.Coprime.Lemmas
 
 /-!
 # Lemmas about units in `ZMod`.

Mathlib/NumberTheory/Padics/RingHoms.lean

@@ -3,8 +3,8 @@ 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.Data.ZMod.Basic
 import Mathlib.NumberTheory.Padics.PadicIntegers
+import Mathlib.RingTheory.ZMod
 
 #align_import number_theory.padics.ring_homs from "leanprover-community/mathlib"@"565eb991e264d0db702722b4bde52ee5173c9950"
 

Mathlib/RingTheory/ZMod.lean

@@ -12,14 +12,32 @@ import Mathlib.RingTheory.PrincipalIdealDomain
 /-!
 # Ring theoretic facts about `ZMod n`
 
-We collect a few facts about `ZMod n` that need some ring theory to be proved/stated
+We collect a few facts about `ZMod n` that need some ring theory to be proved/stated.
 
 ## Main statements
 
-* `isReduced_zmod` - `ZMod n` is reduced for all squarefree `n`.
+* `ZMod.ker_intCastRingHom`:  the ring homomorphism `ℤ → ZMod n` has kernel generated by `n`.
+* `ZMod.ringHom_eq_of_ker_eq`: two ring homomorphisms into `ZMod n` with equal kernels are equal.
+* `isReduced_zmod`: `ZMod n` is reduced for all squarefree `n`.
 -/
 
-
+/-- The ring homomorphism `ℤ → ZMod n` has kernel generated by `n`. -/
+theorem ZMod.ker_intCastRingHom (n : ℕ) :
+    RingHom.ker (Int.castRingHom (ZMod n)) = Ideal.span ({(n : ℤ)} : Set ℤ) := by
+  ext
+  rw [Ideal.mem_span_singleton, RingHom.mem_ker, Int.coe_castRingHom,
+    ZMod.intCast_zmod_eq_zero_iff_dvd]
+#align zmod.ker_int_cast_ring_hom ZMod.ker_intCastRingHom
+
+/-- Two ring homomorphisms into `ZMod n` with equal kernels are equal. -/
+theorem ZMod.ringHom_eq_of_ker_eq {n : ℕ} {R : Type*} [CommRing R] (f g : R →+* ZMod n)
+    (h : RingHom.ker f = RingHom.ker g) : f = g := by
+  have := f.liftOfRightInverse_comp _ (ZMod.ringHom_rightInverse f) ⟨g, le_of_eq h⟩
+  rw [Subtype.coe_mk] at this
+  rw [← this, RingHom.ext_zmod (f.liftOfRightInverse _ _ ⟨g, _⟩) _, RingHom.id_comp]
+#align zmod.ring_hom_eq_of_ker_eq ZMod.ringHom_eq_of_ker_eq
+
+/-- `ZMod n` is reduced iff `n` is square-free (or `n=0`). -/
 @[simp]
 theorem isReduced_zmod {n : ℕ} : IsReduced (ZMod n) ↔ Squarefree n ∨ n = 0 := by
   rw [← RingHom.ker_isRadical_iff_reduced_of_surjective

Mathlib/Topology/Instances/Real.lean

@@ -3,10 +3,11 @@ 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.Algebra.Basic
 import Mathlib.Algebra.Periodic
+import Mathlib.Topology.Algebra.Order.Field
 import Mathlib.Topology.Algebra.UniformMulAction
 import Mathlib.Topology.Algebra.Star
-import Mathlib.Topology.Algebra.Order.Field
 import Mathlib.Topology.Instances.Int
 
 #align_import topology.instances.real from "leanprover-community/mathlib"@"9a59dcb7a2d06bf55da57b9030169219980660cd"