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

• 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.

theorem ZMod.ker_intCastRingHom (n : ℕ) : RingHom.ker (Int.castRingHom (ZMod n)) = Ideal.span {↑n}

The ring homomorphism ℤ → ZMod n has kernel generated by n.

theorem ZMod.ringHom_eq_of_ker_eq {n : ℕ} {R : Type u_1} [Ring R] (f g : R →+* ZMod n) (h : RingHom.ker f = RingHom.ker g) : f = g

Two ring homomorphisms into ZMod n with equal kernels are equal.

@[simp]

theorem isReduced_zmod {n : ℕ} : IsReduced (ZMod n) ↔ Squarefree n ∨ n = 0

ZMod n is reduced iff n is square-free (or n=0).

instance instIsReducedZModOfFactSquarefreeNat {n : ℕ} [Fact (Squarefree n)] : IsReduced (ZMod n)