mathlib3 documentation

data.zmod.basic

Integers mod n #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Definitions #

@[protected, instance]
def zmod.val {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.val_min_abs for a variant that takes values in the integers.

Equations
theorem zmod.val_lt {n : } [ne_zero n] (a : zmod n) :
a.val < n
theorem zmod.val_le {n : } [ne_zero n] (a : zmod n) :
a.val n
@[simp]
theorem zmod.val_zero {n : } :
0.val = 0
@[simp]
theorem zmod.val_one'  :
1.val = 1
@[simp]
theorem zmod.val_neg' {n : zmod 0} :
(-n).val = n.val
@[simp]
theorem zmod.val_mul' {m n : zmod 0} :
(m * n).val = m.val * n.val
theorem zmod.val_nat_cast {n : } (a : ) :
a.val = a % n
@[protected, instance]
def zmod.char_p (n : ) :
char_p (zmod n) n
@[simp]
theorem zmod.add_order_of_one (n : ) :
@[simp]
theorem zmod.add_order_of_coe (a : ) {n : } (n0 : n 0) :

This lemma works in the case in which zmod n is not infinite, i.e. n ≠ 0. The version where a ≠ 0 is add_order_of_coe'.

@[simp]
theorem zmod.add_order_of_coe' {a : } (n : ) (a0 : a 0) :

This lemma works in the case in which a ≠ 0. The version where zmod n is not infinite, i.e. n ≠ 0, is add_order_of_coe.

theorem zmod.ring_char_zmod_n (n : ) :

We have that ring_char (zmod n) = n.

@[simp]
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} [add_group_with_one R] {n : } :
zmod n R

Cast an integer modulo n to another semiring. This function is a morphism if the characteristic of R divides n. See zmod.cast_hom for a bundled version.

Equations
@[protected, instance]
def zmod.has_coe_t {R : Type u_1} [add_group_with_one R] (n : ) :
Equations
@[simp]
theorem zmod.cast_zero {n : } {R : Type u_1} [add_group_with_one R] :
0 = 0
theorem zmod.cast_eq_val {n : } {R : Type u_1} [add_group_with_one R] [ne_zero n] (a : zmod n) :
a = (a.val)
@[simp]
theorem prod.fst_zmod_cast {n : } {R : Type u_1} [add_group_with_one R] {S : Type u_2} [add_group_with_one S] (a : zmod n) :
@[simp]
theorem prod.snd_zmod_cast {n : } {R : Type u_1} [add_group_with_one R] {S : Type u_2} [add_group_with_one S] (a : zmod n) :
theorem zmod.nat_cast_zmod_val {n : } [ne_zero n] (a : zmod n) :
(a.val) = a

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

@[norm_cast]
theorem zmod.int_cast_zmod_cast {n : } (a : zmod n) :

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

@[norm_cast]
theorem zmod.cast_id (n : ) (i : zmod n) :
i = i
@[simp]
theorem zmod.cast_id' {n : } :
@[simp]
theorem zmod.nat_cast_comp_val {n : } (R : Type u_1) [ring R] [ne_zero n] :

The coercions are respectively nat.cast and zmod.cast.

@[simp]
theorem zmod.int_cast_comp_cast {n : } (R : Type u_1) [ring R] :

The coercions are respectively int.cast, zmod.cast, and zmod.cast.

@[simp]
theorem zmod.nat_cast_val {n : } {R : Type u_1} [ring R] [ne_zero n] (i : zmod n) :
(i.val) = i
@[simp]
theorem zmod.int_cast_cast {n : } {R : Type u_1} [ring R] (i : zmod n) :
theorem zmod.coe_add_eq_ite {n : } (a b : zmod n) :
(a + b) = ite (n a + b) (a + b - n) (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 : } [char_p R m] (h : m n) :
1 = 1
theorem zmod.cast_add {n : } {R : Type u_1} [ring R] {m : } [char_p R m] (h : m n) (a b : zmod n) :
(a + b) = a + b
theorem zmod.cast_mul {n : } {R : Type u_1} [ring R] {m : } [char_p R m] (h : m n) (a b : zmod n) :
(a * b) = a * b
def zmod.cast_hom {n m : } (h : m n) (R : Type u_1) [ring R] [char_p 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 add_groups.

Equations
@[simp]
theorem zmod.cast_hom_apply {n : } {R : Type u_1} [ring R] {m : } [char_p R m] {h : m n} (i : zmod n) :
@[simp, norm_cast]
theorem zmod.cast_sub {n : } {R : Type u_1} [ring R] {m : } [char_p R m] (h : m n) (a b : zmod n) :
(a - b) = a - b
@[simp, norm_cast]
theorem zmod.cast_neg {n : } {R : Type u_1} [ring R] {m : } [char_p R m] (h : m n) (a : zmod n) :
@[simp, norm_cast]
theorem zmod.cast_pow {n : } {R : Type u_1} [ring R] {m : } [char_p R m] (h : m n) (a : zmod n) (k : ) :
(a ^ k) = a ^ k
@[simp, norm_cast]
theorem zmod.cast_nat_cast {n : } {R : Type u_1} [ring R] {m : } [char_p R m] (h : m n) (k : ) :
@[simp, norm_cast]
theorem zmod.cast_int_cast {n : } {R : Type u_1} [ring R] {m : } [char_p R m] (h : m n) (k : ) :

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

@[simp]
theorem zmod.cast_one' {n : } {R : Type u_1} [ring R] [char_p R n] :
1 = 1
@[simp]
theorem zmod.cast_add' {n : } {R : Type u_1} [ring R] [char_p R n] (a b : zmod n) :
(a + b) = a + b
@[simp]
theorem zmod.cast_mul' {n : } {R : Type u_1} [ring R] [char_p R n] (a b : zmod n) :
(a * b) = a * b
@[simp]
theorem zmod.cast_sub' {n : } {R : Type u_1} [ring R] [char_p R n] (a b : zmod n) :
(a - b) = a - b
@[simp]
theorem zmod.cast_pow' {n : } {R : Type u_1} [ring R] [char_p R n] (a : zmod n) (k : ) :
(a ^ k) = a ^ k
@[simp, norm_cast]
theorem zmod.cast_nat_cast' {n : } {R : Type u_1} [ring R] [char_p R n] (k : ) :
@[simp, norm_cast]
theorem zmod.cast_int_cast' {n : } {R : Type u_1} [ring R] [char_p R n] (k : ) :
theorem zmod.cast_hom_bijective {n : } (R : Type u_1) [ring R] [char_p R n] [fintype R] (h : fintype.card R = n) :
noncomputable def zmod.ring_equiv {n : } (R : Type u_1) [ring R] [char_p R n] [fintype R] (h : fintype.card R = n) :

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

Equations
def zmod.ring_equiv_congr {m n : } (h : m = n) :

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

Equations
theorem zmod.int_coe_eq_int_coe_iff (a b : ) (c : ) :
theorem zmod.int_coe_eq_int_coe_iff' (a b : ) (c : ) :
a = b a % c = b % c
theorem zmod.nat_coe_eq_nat_coe_iff (a b c : ) :
a = b a b [MOD c]
theorem zmod.nat_coe_eq_nat_coe_iff' (a b c : ) :
a = b a % c = b % c
theorem zmod.int_coe_zmod_eq_zero_iff_dvd (a : ) (b : ) :
a = 0 b a
theorem zmod.int_coe_eq_int_coe_iff_dvd_sub (a b : ) (c : ) :
a = b c b - a
theorem zmod.val_int_cast {n : } (a : ) [ne_zero n] :
(a.val) = a % n
theorem zmod.coe_int_cast {n : } (a : ) :
@[simp]
theorem zmod.val_neg_one (n : ) :
(-1).val = 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) = ite (k = 0) n k - 1
theorem zmod.nat_coe_zmod_eq_iff (p n : ) (z : zmod p) [ne_zero p] :
n = z (k : ), n = z.val + p * k
theorem zmod.int_coe_zmod_eq_iff (p : ) (n : ) (z : zmod p) [ne_zero p] :
n = z (k : ), n = (z.val) + p * k
@[simp]
theorem zmod.int_cast_mod (a : ) (b : ) :
(a % b) = a
@[simp]
theorem zmod.nat_cast_to_nat (p : ) {z : } (h : 0 z) :
theorem zmod.val_one_eq_one_mod (n : ) :
1.val = 1 % n
theorem zmod.val_one (n : ) [fact (1 < n)] :
1.val = 1
theorem zmod.val_add {n : } [ne_zero n] (a b : zmod n) :
(a + b).val = (a.val + b.val) % n
theorem zmod.val_mul {n : } (a b : zmod n) :
(a * b).val = a.val * b.val % n
@[protected, instance]
def zmod.nontrivial (n : ) [fact (1 < n)] :
@[protected, instance]
def zmod.inv (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.

Equations
@[protected, instance]
def zmod.has_inv (n : ) :
Equations
theorem zmod.inv_zero (n : ) :
0⁻¹ = 0
theorem zmod.mul_inv_eq_gcd {n : } (a : zmod n) :
a * a⁻¹ = (a.val.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.coprime n) :
x * (x)⁻¹ = 1
def zmod.unit_of_coprime {n : } (x : ) (h : x.coprime n) :
(zmod n)ˣ

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

Equations
@[simp]
theorem zmod.coe_unit_of_coprime {n : } (x : ) (h : x.coprime n) :
theorem zmod.val_coe_unit_coprime {n : } (u : (zmod n)ˣ) :
@[simp]
theorem zmod.inv_coe_unit {n : } (u : (zmod n)ˣ) :
theorem zmod.mul_inv_of_unit {n : } (a : zmod n) (h : is_unit a) :
a * a⁻¹ = 1
theorem zmod.inv_mul_of_unit {n : } (a : zmod n) (h : is_unit a) :
a⁻¹ * a = 1
def zmod.units_equiv_coprime {n : } [ne_zero n] :
(zmod n)ˣ {x // x.val.coprime n}

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

Equations
def zmod.chinese_remainder {m n : } (h : m.coprime n) :
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.quotient_inf_ring_equiv_pi_quotient for the Chinese remainder theorem for ideals in any ring.

Equations
@[protected, instance]
theorem zmod.le_div_two_iff_lt_neg (n : ) [hn : fact (n % 2 = 1)] {x : zmod n} (hx0 : x 0) :
x.val n / 2 n / 2 < (-x).val
theorem zmod.ne_neg_self (n : ) [hn : fact (n % 2 = 1)] {a : zmod n} (ha : a 0) :
a -a
theorem zmod.neg_one_ne_one {n : } [fact (2 < n)] :
-1 1
theorem zmod.neg_eq_self_mod_two (a : zmod 2) :
-a = a
@[simp]
theorem zmod.nat_abs_mod_two (a : ) :
@[simp]
theorem zmod.val_eq_zero {n : } (a : zmod n) :
a.val = 0 a = 0
theorem zmod.neg_eq_self_iff {n : } (a : zmod n) :
-a = a a = 0 2 * a.val = n
theorem zmod.val_cast_of_lt {n a : } (h : a < n) :
a.val = a
theorem zmod.neg_val' {n : } [ne_zero n] (a : zmod n) :
(-a).val = (n - a.val) % n
theorem zmod.neg_val {n : } [ne_zero n] (a : zmod n) :
(-a).val = ite (a = 0) 0 (n - a.val)
def zmod.val_min_abs {n : } :

val_min_abs 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].

Equations
@[simp]
theorem zmod.val_min_abs_def_zero (x : zmod 0) :
theorem zmod.val_min_abs_def_pos {n : } [ne_zero n] (x : zmod n) :
x.val_min_abs = ite (x.val n / 2) (x.val) ((x.val) - n)
@[simp, norm_cast]
theorem zmod.coe_val_min_abs {n : } (x : zmod n) :
theorem nat.le_div_two_iff_mul_two_le {n m : } :
m n / 2 m * 2 n
theorem zmod.val_min_abs_nonneg_iff {n : } [ne_zero n] (x : zmod n) :
theorem zmod.val_min_abs_mul_two_eq_iff {n : } (a : zmod n) :
a.val_min_abs * 2 = n 2 * a.val = n
theorem zmod.val_min_abs_mem_Ioc {n : } [ne_zero n] (x : zmod n) :
theorem zmod.val_min_abs_spec {n : } [ne_zero n] (x : zmod n) (y : ) :
@[simp]
theorem zmod.val_min_abs_zero (n : ) :
@[simp]
theorem zmod.val_min_abs_eq_zero {n : } (x : zmod n) :
x.val_min_abs = 0 x = 0
theorem zmod.nat_cast_nat_abs_val_min_abs {n : } [ne_zero n] (a : zmod n) :
(a.val_min_abs.nat_abs) = ite (a.val n / 2) a (-a)
theorem zmod.val_min_abs_neg_of_ne_half {n : } {a : zmod n} (ha : 2 * a.val n) :
theorem zmod.val_eq_ite_val_min_abs {n : } [ne_zero n] (a : zmod n) :
(a.val) = a.val_min_abs + ite (a.val n / 2) 0 n
theorem zmod.prime_ne_zero (p q : ) [hp : fact (nat.prime p)] [hq : fact (nat.prime q)] (hpq : p q) :
q 0
theorem zmod.val_min_abs_nat_cast_of_half_lt {n a : } (ha : n / 2 < a) (ha' : a < n) :
theorem zmod.nat_abs_min_of_le_div_two (n : ) (x y : ) (he : x = y) (hl : x.nat_abs n / 2) :
@[protected, instance]
def zmod.field (p : ) [fact (nat.prime p)] :

Field structure on zmod p if p is prime.

Equations
@[protected, instance]
def zmod.is_domain (p : ) [hp : fact (nat.prime p)] :

zmod p is an integral domain when p is prime.

theorem ring_hom.ext_zmod {n : } {R : Type u_1} [semiring R] (f g : zmod n →+* R) :
f = g
@[protected, instance]
@[protected, instance]
@[simp]
theorem zmod.ring_hom_map_cast {n : } {R : Type u_1} [ring R] (f : R →+* zmod n) (k : zmod n) :
f k = k
theorem zmod.ring_hom_surjective {n : } {R : Type u_1} [ring R] (f : R →+* zmod n) :
theorem zmod.ring_hom_eq_of_ker_eq {n : } {R : Type u_1} [comm_ring R] (f g : R →+* zmod n) (h : ring_hom.ker f = ring_hom.ker g) :
f = g
def zmod.lift (n : ) {A : Type u_2} [add_group A] :
{f // f n = 0} (zmod n →+ A)

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

Equations
@[simp]
theorem zmod.lift_symm_apply_coe_apply (n : ) {A : Type u_2} [add_group A] (ᾰ : zmod n →+ A) (ᾰ_1 : ) :
(((zmod.lift n).symm) ᾰ) ᾰ_1 = ᾰ_1
@[simp]
theorem zmod.lift_apply_apply (n : ) {A : Type u_2} [add_group A] (ᾰ : {x // x n = 0}) (b : zmod n) :
((zmod.lift n) ᾰ) b = b
@[simp]
theorem zmod.lift_coe (n : ) {A : Type u_2} [add_group A] (f : {f // f n = 0}) (x : ) :
((zmod.lift n) f) x = f x
theorem zmod.lift_cast_add_hom (n : ) {A : Type u_2} [add_group A] (f : {f // f n = 0}) (x : ) :
@[simp]
theorem zmod.lift_comp_coe (n : ) {A : Type u_2} [add_group A] (f : {f // f n = 0}) :
@[simp]
theorem zmod.lift_comp_cast_add_hom (n : ) {A : Type u_2} [add_group A] (f : {f // f n = 0}) :