# Documentation

Mathlib.Data.ZMod.Basic

# Integers mod n#

Definition of the integers mod n, and the field structure on the integers mod p.

## Definitions #

• ZMod n, which is for integers modulo a nat n : ℕ

• val a is defined as a natural number:

• for a : ZMod 0 it is the absolute value of a
• for a : ZMod n with 0 < n it is the least natural number in the equivalence class
• valMinAbs returns the integer closest to zero in the equivalence class.

• A coercion cast is defined from ZMod n into any ring. This is a ring hom if the ring has characteristic dividing n

def ZMod.val {n : } :
ZMod n

val a is a natural number defined as:

• for a : ZMod 0 it is the absolute value of a
• for a : ZMod n with 0 < n it is the least natural number in the equivalence class

See ZMod.valMinAbs for a variant that takes values in the integers.

Instances For
theorem ZMod.val_lt {n : } [] (a : ZMod n) :
< n
theorem ZMod.val_le {n : } [] (a : ZMod n) :
n
@[simp]
theorem ZMod.val_zero {n : } :
= 0
@[simp]
theorem ZMod.val_one' :
= 1
@[simp]
theorem ZMod.val_neg' {n : ZMod 0} :
@[simp]
theorem ZMod.val_mul' {m : ZMod 0} {n : ZMod 0} :
ZMod.val (m * n) =
theorem ZMod.val_nat_cast {n : } (a : ) :
ZMod.val a = a % n
instance ZMod.charP (n : ) :
CharP (ZMod n) n
@[simp]
theorem ZMod.addOrderOf_one (n : ) :
= n
@[simp]
theorem ZMod.addOrderOf_coe (a : ) {n : } (n0 : n 0) :
= n / Nat.gcd n a

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'.

@[simp]
theorem ZMod.addOrderOf_coe' {a : } (n : ) (a0 : a 0) :
= n / Nat.gcd n a

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.

theorem ZMod.ringChar_zmod_n (n : ) :

We have that ringChar (ZMod n) = n.

theorem ZMod.nat_cast_self (n : ) :
n = 0
@[simp]
theorem ZMod.nat_cast_self' (n : ) :
n + 1 = 0
def ZMod.cast {R : Type u_1} [] {n : } :
ZMod nR

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
instance ZMod.instCoeTCZMod {R : Type u_1} [] (n : ) :
CoeTC (ZMod n) R
@[simp]
theorem ZMod.cast_zero {n : } {R : Type u_1} [] :
0 = 0
theorem ZMod.cast_eq_val {n : } {R : Type u_1} [] [] (a : ZMod n) :
a = ↑()
@[simp]
theorem Prod.fst_zmod_cast {n : } {R : Type u_1} [] {S : Type u_2} [] (a : ZMod n) :
(a).fst = a
@[simp]
theorem Prod.snd_zmod_cast {n : } {R : Type u_1} [] {S : Type u_2} [] (a : ZMod n) :
(a).snd = a
theorem ZMod.nat_cast_zmod_val {n : } [] (a : ZMod n) :
↑() = a

So-named because the coercion is Nat.cast into ZMod. For Nat.cast into an arbitrary ring, see ZMod.nat_cast_val.

theorem ZMod.nat_cast_rightInverse {n : } [] :
Function.RightInverse ZMod.val Nat.cast
theorem ZMod.int_cast_zmod_cast {n : } (a : ZMod n) :
a = a

So-named because the outer coercion is Int.cast into ZMod. For Int.cast into an arbitrary ring, see ZMod.int_cast_cast.

theorem ZMod.cast_id (n : ) (i : ZMod n) :
i = i
@[simp]
theorem ZMod.cast_id' {n : } :
ZMod.cast = id
@[simp]
theorem ZMod.nat_cast_comp_val {n : } (R : Type u_1) [Ring R] [] :
Nat.cast ZMod.val = ZMod.cast

The coercions are respectively Nat.cast and ZMod.cast.

@[simp]
theorem ZMod.int_cast_comp_cast {n : } (R : Type u_1) [Ring R] :
Int.cast ZMod.cast = ZMod.cast

The coercions are respectively Int.cast, ZMod.cast, and ZMod.cast.

@[simp]
theorem ZMod.nat_cast_val {n : } {R : Type u_1} [Ring R] [] (i : ZMod n) :
↑() = i
@[simp]
theorem ZMod.int_cast_cast {n : } {R : Type u_1} [Ring R] (i : ZMod n) :
i = i
theorem ZMod.coe_add_eq_ite {n : } (a : ZMod n) (b : ZMod n) :
↑(a + b) = if n a + b then a + b - n else a + b

If the characteristic of R divides n, then cast is a homomorphism.

@[simp]
theorem ZMod.cast_one {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) :
1 = 1
theorem ZMod.cast_add {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (a : ZMod n) (b : ZMod n) :
↑(a + b) = a + b
theorem ZMod.cast_mul {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (a : ZMod n) (b : ZMod n) :
↑(a * b) = a * b
def ZMod.castHom {n : } {m : } (h : m n) (R : Type u_2) [Ring R] [CharP R m] :

The canonical ring homomorphism from ZMod n to a ring of characteristic n.

See also ZMod.lift (in Data.ZMod.Quotient) for a generalized version working in AddGroups.

Instances For
@[simp]
theorem ZMod.castHom_apply {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] {h : m n} (i : ZMod n) :
↑() i = i
@[simp]
theorem ZMod.cast_sub {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (a : ZMod n) (b : ZMod n) :
↑(a - b) = a - b
@[simp]
theorem ZMod.cast_neg {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (a : ZMod n) :
↑(-a) = -a
@[simp]
theorem ZMod.cast_pow {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (a : ZMod n) (k : ) :
↑(a ^ k) = a ^ k
@[simp]
theorem ZMod.cast_nat_cast {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (k : ) :
k = k
@[simp]
theorem ZMod.cast_int_cast {n : } {R : Type u_1} [Ring R] {m : } [CharP R m] (h : m n) (k : ) :
k = k

Some specialised simp lemmas which apply when R has characteristic n.

@[simp]
theorem ZMod.cast_one' {n : } {R : Type u_1} [Ring R] [CharP R n] :
1 = 1
@[simp]
theorem ZMod.cast_add' {n : } {R : Type u_1} [Ring R] [CharP R n] (a : ZMod n) (b : ZMod n) :
↑(a + b) = a + b
@[simp]
theorem ZMod.cast_mul' {n : } {R : Type u_1} [Ring R] [CharP R n] (a : ZMod n) (b : ZMod n) :
↑(a * b) = a * b
@[simp]
theorem ZMod.cast_sub' {n : } {R : Type u_1} [Ring R] [CharP R n] (a : ZMod n) (b : ZMod n) :
↑(a - b) = a - b
@[simp]
theorem ZMod.cast_pow' {n : } {R : Type u_1} [Ring R] [CharP R n] (a : ZMod n) (k : ) :
↑(a ^ k) = a ^ k
@[simp]
theorem ZMod.cast_nat_cast' {n : } {R : Type u_1} [Ring R] [CharP R n] (k : ) :
k = k
@[simp]
theorem ZMod.cast_int_cast' {n : } {R : Type u_1} [Ring R] [CharP R n] (k : ) :
k = k
theorem ZMod.castHom_injective {n : } (R : Type u_1) [Ring R] [CharP R n] :
theorem ZMod.castHom_bijective {n : } (R : Type u_1) [Ring R] [CharP R n] [] (h : ) :
noncomputable def ZMod.ringEquiv {n : } (R : Type u_1) [Ring R] [CharP R n] [] (h : ) :

The unique ring isomorphism between ZMod n and a ring R of characteristic n and cardinality n.

Instances For
def ZMod.ringEquivCongr {m : } {n : } (h : m = n) :

The identity between ZMod m and ZMod n when m = n, as a ring isomorphism.

Instances For
theorem ZMod.int_cast_eq_int_cast_iff (a : ) (b : ) (c : ) :
a = b a b [ZMOD c]
theorem ZMod.int_cast_eq_int_cast_iff' (a : ) (b : ) (c : ) :
a = b a % c = b % c
theorem ZMod.nat_cast_eq_nat_cast_iff (a : ) (b : ) (c : ) :
a = b a b [MOD c]
theorem ZMod.nat_cast_eq_nat_cast_iff' (a : ) (b : ) (c : ) :
a = b a % c = b % c
theorem ZMod.int_cast_zmod_eq_zero_iff_dvd (a : ) (b : ) :
a = 0 b a
theorem ZMod.int_cast_eq_int_cast_iff_dvd_sub (a : ) (b : ) (c : ) :
a = b c b - a
theorem ZMod.nat_cast_zmod_eq_zero_iff_dvd (a : ) (b : ) :
a = 0 b a
theorem ZMod.val_int_cast {n : } (a : ) [] :
↑(ZMod.val a) = a % n
theorem ZMod.coe_int_cast {n : } (a : ) :
a = a % n
@[simp]
theorem ZMod.val_neg_one (n : ) :
ZMod.val (-1) = n
theorem ZMod.cast_neg_one {R : Type u_1} [Ring R] (n : ) :
↑(-1) = n - 1

-1 : ZMod n lifts to n - 1 : R. This avoids the characteristic assumption in cast_neg.

theorem ZMod.cast_sub_one {R : Type u_1} [Ring R] {n : } (k : ZMod n) :
↑(k - 1) = (if k = 0 then n else k) - 1
theorem ZMod.nat_coe_zmod_eq_iff (p : ) (n : ) (z : ZMod p) [] :
n = z k, n = + p * k
theorem ZMod.int_coe_zmod_eq_iff (p : ) (n : ) (z : ZMod p) [] :
n = z k, n = ↑() + p * k
@[simp]
theorem ZMod.int_cast_mod (a : ) (b : ) :
↑(a % b) = a
@[simp]
theorem ZMod.nat_cast_toNat (p : ) {z : } (_h : 0 z) :
↑() = z
theorem ZMod.val_one_eq_one_mod (n : ) :
= 1 % n
theorem ZMod.val_one (n : ) [Fact (1 < n)] :
= 1
theorem ZMod.val_add {n : } [] (a : ZMod n) (b : ZMod n) :
ZMod.val (a + b) = () % n
theorem ZMod.val_mul {n : } (a : ZMod n) (b : ZMod n) :
ZMod.val (a * b) = % n
instance ZMod.nontrivial (n : ) [Fact (1 < n)] :
def ZMod.inv (n : ) :
ZMod nZMod n

The inversion on ZMod n. It is setup in such a way that a * a⁻¹ is equal to gcd a.val n. In particular, if a is coprime to n, and hence a unit, a * a⁻¹ = 1.

Instances For
instance ZMod.instInvZMod (n : ) :
Inv (ZMod n)
theorem ZMod.inv_zero (n : ) :
0⁻¹ = 0
theorem ZMod.mul_inv_eq_gcd {n : } (a : ZMod n) :
a * a⁻¹ = ↑(Nat.gcd () n)
@[simp]
theorem ZMod.nat_cast_mod (a : ) (n : ) :
↑(a % n) = a
theorem ZMod.eq_iff_modEq_nat (n : ) {a : } {b : } :
a = b a b [MOD n]
theorem ZMod.coe_mul_inv_eq_one {n : } (x : ) (h : ) :
x * (x)⁻¹ = 1
def ZMod.unitOfCoprime {n : } (x : ) (h : ) :
(ZMod n)ˣ

unitOfCoprime makes an element of (ZMod n)ˣ given a natural number x and a proof that x is coprime to n

Instances For
@[simp]
theorem ZMod.coe_unitOfCoprime {n : } (x : ) (h : ) :
↑() = x
@[simp]
theorem ZMod.inv_coe_unit {n : } (u : (ZMod n)ˣ) :
(u)⁻¹ = u⁻¹
theorem ZMod.mul_inv_of_unit {n : } (a : ZMod n) (h : ) :
a * a⁻¹ = 1
theorem ZMod.inv_mul_of_unit {n : } (a : ZMod n) (h : ) :
a⁻¹ * a = 1
def ZMod.unitsEquivCoprime {n : } [] :
(ZMod n)ˣ { x // Nat.Coprime () n }

Equivalence between the units of ZMod n and the subtype of terms x : ZMod n for which x.val is coprime to n

Instances For
def ZMod.chineseRemainder {m : } {n : } (h : ) :
ZMod (m * n) ≃+* ZMod m × ZMod n

The Chinese remainder theorem. For a pair of coprime natural numbers, m and n, the rings ZMod (m * n) and ZMod m × ZMod n are isomorphic.

See Ideal.quotientInfRingEquivPiQuotient for the Chinese remainder theorem for ideals in any ring.

Instances For
@[simp]
theorem ZMod.add_self_eq_zero_iff_eq_zero {n : } (hn : Odd n) {a : ZMod n} :
a + a = 0 a = 0
theorem ZMod.ne_neg_self {n : } (hn : Odd n) {a : ZMod n} (ha : a 0) :
a -a
theorem ZMod.neg_one_ne_one {n : } [Fact (2 < n)] :
-1 1
@[simp]
theorem ZMod.natAbs_mod_two (a : ) :
↑() = a
@[simp]
theorem ZMod.val_eq_zero {n : } (a : ZMod n) :
= 0 a = 0
theorem ZMod.neg_eq_self_iff {n : } (a : ZMod n) :
-a = a a = 0 2 * = n
theorem ZMod.val_cast_of_lt {n : } {a : } (h : a < n) :
ZMod.val a = a
theorem ZMod.neg_val' {n : } [] (a : ZMod n) :
ZMod.val (-a) = (n - ) % n
theorem ZMod.neg_val {n : } [] (a : ZMod n) :
ZMod.val (-a) = if a = 0 then 0 else n -
def ZMod.valMinAbs {n : } :
ZMod n

valMinAbs x returns the integer in the same equivalence class as x that is closest to 0, The result will be in the interval (-n/2, n/2].

Instances For
@[simp]
theorem ZMod.valMinAbs_def_zero (x : ZMod 0) :
theorem ZMod.valMinAbs_def_pos {n : } [] (x : ZMod n) :
= if n / 2 then ↑() else ↑() - n
@[simp]
theorem ZMod.coe_valMinAbs {n : } (x : ZMod n) :
↑() = x
theorem Nat.le_div_two_iff_mul_two_le {n : } {m : } :
m n / 2 m * 2 n
theorem ZMod.valMinAbs_nonneg_iff {n : } [] (x : ZMod n) :
n / 2
theorem ZMod.valMinAbs_mul_two_eq_iff {n : } (a : ZMod n) :
= n 2 * = n
theorem ZMod.valMinAbs_mem_Ioc {n : } [] (x : ZMod n) :
Set.Ioc (-n) n
theorem ZMod.valMinAbs_spec {n : } [] (x : ZMod n) (y : ) :
x = y y * 2 Set.Ioc (-n) n
theorem ZMod.natAbs_valMinAbs_le {n : } [] (x : ZMod n) :
n / 2
@[simp]
theorem ZMod.valMinAbs_zero (n : ) :
@[simp]
theorem ZMod.valMinAbs_eq_zero {n : } (x : ZMod n) :
x = 0
theorem ZMod.nat_cast_natAbs_valMinAbs {n : } [] (a : ZMod n) :
↑() = if n / 2 then a else -a
theorem ZMod.valMinAbs_neg_of_ne_half {n : } {a : ZMod n} (ha : 2 * n) :
@[simp]
theorem ZMod.natAbs_valMinAbs_neg {n : } (a : ZMod n) :
theorem ZMod.val_eq_ite_valMinAbs {n : } [] (a : ZMod n) :
↑() = + ↑(if n / 2 then 0 else n)
theorem ZMod.prime_ne_zero (p : ) (q : ) [hp : Fact ()] [hq : Fact ()] (hpq : p q) :
q 0
theorem ZMod.valMinAbs_natAbs_eq_min {n : } [hpos : ] (a : ZMod n) :
= min () (n - )
theorem ZMod.valMinAbs_natCast_of_le_half {n : } {a : } (ha : a n / 2) :
= a
theorem ZMod.valMinAbs_natCast_of_half_lt {n : } {a : } (ha : n / 2 < a) (ha' : a < n) :
= a - n
@[simp]
theorem ZMod.valMinAbs_natCast_eq_self {n : } {a : } [] :
= a a n / 2
theorem ZMod.natAbs_min_of_le_div_two (n : ) (x : ) (y : ) (he : x = y) (hl : n / 2) :
instance ZMod.instFieldZMod (p : ) [Fact ()] :

Field structure on ZMod p if p is prime.

ZMod p is an integral domain when p is prime.

theorem RingHom.ext_zmod {n : } {R : Type u_1} [] (f : ZMod n →+* R) (g : ZMod n →+* R) :
f = g
instance ZMod.subsingleton_ringHom {n : } {R : Type u_1} [] :
@[simp]
theorem ZMod.ringHom_map_cast {n : } {R : Type u_1} [Ring R] (f : R →+* ZMod n) (k : ZMod n) :
f k = k
theorem ZMod.ringHom_rightInverse {n : } {R : Type u_1} [Ring R] (f : R →+* ZMod n) :
Function.RightInverse ZMod.cast f
theorem ZMod.ringHom_surjective {n : } {R : Type u_1} [Ring R] (f : R →+* ZMod n) :
theorem ZMod.ringHom_eq_of_ker_eq {n : } {R : Type u_1} [] (f : R →+* ZMod n) (g : R →+* ZMod n) (h : ) :
f = g
@[simp]
theorem ZMod.castHom_self {n : } :
ZMod.castHom (_ : n n) (ZMod n) = RingHom.id (ZMod n)
@[simp]
theorem ZMod.castHom_comp {n : } {m : } {d : } (hm : n m) (hd : m d) :
def ZMod.lift (n : ) {A : Type u_2} [] :
{ f // f n = 0 } (ZMod n →+ A)

The map from ZMod n induced by f : ℤ →+ A that maps n to 0.

Instances For
@[simp]
theorem ZMod.lift_coe (n : ) {A : Type u_2} [] (f : { f // f n = 0 }) (x : ) :
↑(↑() f) x = f x
theorem ZMod.lift_castAddHom (n : ) {A : Type u_2} [] (f : { f // f n = 0 }) (x : ) :
↑(↑() f) (↑() x) = f x
@[simp]
theorem ZMod.lift_comp_coe (n : ) {A : Type u_2} [] (f : { f // f n = 0 }) :
↑(↑() f) Int.cast = f
@[simp]
theorem ZMod.lift_comp_castAddHom (n : ) {A : Type u_2} [] (f : { f // f n = 0 }) :
AddMonoidHom.comp (↑() f) () = f