feat: port RingTheory.ZMod (#3257)

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Mathlib.lean

@@ -1439,6 +1439,7 @@ import Mathlib.RingTheory.Subsemiring.Pointwise
 import Mathlib.RingTheory.UniqueFactorizationDomain
 import Mathlib.RingTheory.Valuation.Basic
 import Mathlib.RingTheory.Valuation.Integers
+import Mathlib.RingTheory.ZMod
 import Mathlib.SetTheory.Cardinal.Basic
 import Mathlib.SetTheory.Cardinal.Cofinality
 import Mathlib.SetTheory.Cardinal.Continuum

Mathlib/Algebra/Squarefree.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 
 ! This file was ported from Lean 3 source module algebra.squarefree
-! leanprover-community/mathlib commit 79de90f7beca025f469dcda978ae655c4d985946
+! leanprover-community/mathlib commit 00d163e35035c3577c1c79fa53b68de17781ffc1
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -265,3 +265,18 @@ theorem dvd_pow_iff_dvd_of_squarefree {x y : R} {n : ℕ} (hsq : Squarefree x) (
 #align unique_factorization_monoid.dvd_pow_iff_dvd_of_squarefree UniqueFactorizationMonoid.dvd_pow_iff_dvd_of_squarefree
 
 end UniqueFactorizationMonoid
+
+namespace Int
+
+@[simp]
+theorem squarefree_natAbs {n : ℤ} : Squarefree n.natAbs ↔ Squarefree n := by
+  simp_rw [Squarefree, natAbs_surjective.forall, ← natAbs_mul, natAbs_dvd_natAbs,
+    isUnit_iff_natAbs_eq, Nat.isUnit_iff]
+#align int.squarefree_nat_abs Int.squarefree_natAbs
+
+@[simp]
+theorem squarefree_coe_nat {n : ℕ} : Squarefree (n : ℤ) ↔ Squarefree n := by
+  rw [← squarefree_natAbs, natAbs_ofNat]
+#align int.squarefree_coe_nat Int.squarefree_coe_nat
+
+end Int

Mathlib/Data/Int/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 
 ! This file was ported from Lean 3 source module data.int.basic
-! leanprover-community/mathlib commit 728baa2f54e6062c5879a3e397ac6bac323e506f
+! leanprover-community/mathlib commit 00d163e35035c3577c1c79fa53b68de17781ffc1
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -198,6 +198,9 @@ theorem succ_neg_nat_succ (n : ℕ) : succ (-Nat.succ n) = -n := succ_neg_succ n
 
 /-! ### nat abs -/
 
+theorem natAbs_surjective : natAbs.Surjective := fun n => ⟨n, natAbs_ofNat n⟩
+#align int.nat_abs_surjective Int.natAbs_surjective
+
 #align int.nat_abs_add_le Int.natAbs_add_le
 #align int.nat_abs_sub_le Int.natAbs_sub_le
 #align int.nat_abs_neg_of_nat Int.natAbs_negOfNat

Mathlib/RingTheory/ZMod.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2022 Alex J. Best. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alex J. Best
+
+! This file was ported from Lean 3 source module ring_theory.zmod
+! leanprover-community/mathlib commit 00d163e35035c3577c1c79fa53b68de17781ffc1
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Algebra.Squarefree
+import Mathlib.Data.ZMod.Basic
+import Mathlib.RingTheory.Int.Basic
+
+/-!
+# Ring theoretic facts about `ZMod n`
+
+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`.
+-/
+
+
+@[simp]
+theorem isReduced_zmod {n : ℕ} : IsReduced (ZMod n) ↔ Squarefree n ∨ n = 0 := by
+  rw [← RingHom.ker_isRadical_iff_reduced_of_surjective
+      (ZMod.ringHom_surjective <| Int.castRingHom <| ZMod n),
+      ZMod.ker_int_castRingHom, ← isRadical_iff_span_singleton, isRadical_iff_squarefree_or_zero,
+      Int.squarefree_coe_nat, Nat.cast_eq_zero]
+#align is_reduced_zmod isReduced_zmod
+
+instance {n : ℕ} [Fact <| Squarefree n] : IsReduced (ZMod n) :=
+  isReduced_zmod.2 <| Or.inl <| Fact.out