English
ZMod n is reduced if and only if n is squarefree or n = 0.
Русский
ZMod n редуцирован тогда и только тогда, когда n квадратно-разделимо или n = 0.
LaTeX
$$$IsReduced(\\\\mathbb{Z}/n\\\\mathbb{Z}) \\\\Leftrightarrow (Squarefree(n) \\\\lor n=0).$$$
Lean4
/-- `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 (ZMod.ringHom_surjective <| Int.castRingHom <| ZMod n),
ZMod.ker_intCastRingHom, ← isRadical_iff_span_singleton, isRadical_iff_squarefree_or_zero, Int.squarefree_natCast,
Nat.cast_eq_zero]
