Documentation

Mathlib.RingTheory.ZMod

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 #

@[simp]
theorem isReduced_zmod {n : } :