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 #

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

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

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

theorem isReduced_zmod {n : } :

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