# 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`

.

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.

@[simp]

`ZMod n`

is reduced iff `n`

is square-free (or `n=0`

).

## Equations

- ⋯ = ⋯