[GOAL]
n : ℕ
⊢ IsReduced (ZMod n) ↔ Squarefree n ∨ n = 0
[PROOFSTEP]
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]
