Definition of the integers mod n, and the field structure on the integers mod p.
ZMod n, which is for integers modulo a nat
n : ℕ
val ais defined as a natural number:
valMinAbsreturns the integer closest to zero in the equivalence class.
If the characteristic of
cast is a homomorphism.
Some specialised simp lemmas which apply when
R has characteristic
Ideal.quotientInfRingEquivPiQuotient for the Chinese remainder theorem for ideals in any