Integers mod n
#
Definition of the integers mod n, and the field structure on the integers mod p.
Definitions #
This lemma works in the case in which ZMod n
is not infinite, i.e. n ≠ 0
. The version
where a ≠ 0
is addOrderOf_coe'
.
This lemma works in the case in which a ≠ 0
. The version where
ZMod n
is not infinite, i.e. n ≠ 0
, is addOrderOf_coe
.
Cast an integer modulo n
to another semiring.
This function is a morphism if the characteristic of R
divides n
.
See ZMod.castHom
for a bundled version.
Instances For
So-named because the outer coercion is Int.cast
into ZMod
. For Int.cast
into an arbitrary
ring, see ZMod.int_cast_cast
.
If the characteristic of R
divides n
, then cast
is a homomorphism.
Some specialised simp lemmas which apply when R
has characteristic n
.
unitOfCoprime
makes an element of (ZMod n)ˣ
given
a natural number x
and a proof that x
is coprime to n