Kernels of homomorphisms to residue rings

A map to ZMod n is determined by its kernel, since the residue ring is generated by the image of the integers. This gives a convenient way to distinguish the ideals arising from different polynomial residue roots.

theorem NairTenenbaum.zmod_ringHom_ker_injective {R : Type u_1} [CommRing R] (n : ℕ) : Function.Injective fun (f : R →+* ZMod n) => RingHom.ker f

theorem NairTenenbaum.cardQuot_ker_zmod {R : Type u_1} [CommRing R] {n : ℕ} (f : R →+* ZMod n) : Submodule.cardQuot (RingHom.ker f) = n