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

• isReduced_zmod - ZMod n is reduced for all squarefree n.

@[simp]

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

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

Equations

• (_ : IsReduced (ZMod n)) = (_ : IsReduced (ZMod n))