mathlib documentation

data.zmod.basic

Integers mod n #

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

Definitions #

Ring structure on fin n #

We define a commutative ring structure on fin n, but we do not register it as instance. Afterwords, when we define zmod n in terms of fin n, we use these definitions to register the ring structure on zmod n as type class instance.

@[instance]
def fin.comm_semigroup (n : ) :

Multiplicative commutative semigroup structure on fin (n+1).

Equations
def zmod  :
→ Type

The integers modulo n : ℕ.

Equations
@[instance]
def zmod.fintype (n : ) [fact (0 < n)] :
Equations
theorem zmod.card (n : ) [fact (0 < n)] :
@[instance]
def zmod.has_repr (n : ) :
Equations
@[instance]
def zmod.comm_ring (n : ) :
Equations
@[instance]
def zmod.inhabited (n : ) :
Equations
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.val_min_abs for a variant that takes values in the integers.

Equations
theorem zmod.val_lt {n : } [fact (0 < 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
@[instance]
def zmod.char_p (n : ) :
char_p (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} [has_zero R] [has_one R] [has_add R] [has_neg 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
@[instance]
def zmod.has_coe_t {R : Type u_1} [has_zero R] [has_one R] [has_add R] [has_neg R] (n : ) :
Equations
@[simp]
theorem zmod.cast_zero {n : } {R : Type u_1} [has_zero R] [has_one R] [has_add R] [has_neg R] :
0 = 0
theorem zmod.nat_cast_zmod_val {n : } [fact (0 < 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.

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.

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] [fact (0 < 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] [fact (0 < 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]
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]
theorem zmod.cast_neg {n : } {R : Type u_1} [ring R] {m : } [char_p R m] (h : m n) (a : zmod n) :
@[simp]
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]
theorem zmod.cast_nat_cast {n : } {R : Type u_1} [ring R] {m : } [char_p R m] (h : m n) (k : ) :
@[simp]
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]
theorem zmod.cast_nat_cast' {n : } {R : Type u_1} [ring R] [char_p R n] (k : ) :
@[simp]
theorem zmod.cast_int_cast' {n : } {R : Type u_1} [ring R] [char_p R n] (k : ) :
@[instance]
def zmod.algebra {n : } (R : Type u_1) [comm_ring R] [char_p R n] :
Equations
theorem zmod.cast_hom_injective {n : } (R : Type u_1) [ring R] [char_p R n] :
theorem zmod.cast_hom_bijective {n : } (R : Type u_1) [ring R] [char_p R n] [fintype R] (h : fintype.card R = n) :
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
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.int_coe_zmod_eq_zero_iff_dvd (a : ) (b : ) :
a = 0 b a
@[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 : } [fact (0 < 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
@[instance]
def 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.

Equations
@[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 (n a : ) :
(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) :

unit_of_coprime makes an element of units (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 : units (zmod n)) :
@[simp]
theorem zmod.inv_coe_unit {n : } (u : units (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 : } [fact (0 < n)] :
units (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
@[simp]
theorem zmod.card_units_eq_totient (n : ) [fact (0 < n)] :
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
@[simp]
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.val_cast_of_lt {n a : } (h : a < n) :
a.val = a
theorem zmod.neg_val' {n : } [fact (0 < n)] (a : zmod n) :
(-a).val = (n - a.val) % n
theorem zmod.neg_val {n : } [fact (0 < n)] (a : zmod n) :
(-a).val = ite (a = 0) 0 (n - a.val)
def zmod.val_min_abs {n : } :
zmod 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 : } [fact (0 < n)] (x : zmod n) :
x.val_min_abs = ite (x.val n / 2) (x.val) ((x.val) - n)
@[simp]
theorem zmod.coe_val_min_abs {n : } (x : zmod n) :
theorem zmod.nat_abs_val_min_abs_le {n : } [fact (0 < n)] (x : zmod n) :
@[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 : } [fact (0 < n)] (a : zmod n) :
(a.val_min_abs.nat_abs) = ite (a.val n / 2) a (-a)
theorem zmod.val_eq_ite_val_min_abs {n : } [fact (0 < 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 ring_hom.ext_zmod {n : } {R : Type u_1} [semiring R] (f g : zmod n →+* R) :
f = g
@[instance]
def zmod.subsingleton_ring_hom {n : } {R : Type u_1} [semiring R] :
@[instance]
def zmod.subsingleton_ring_equiv {n : } {R : Type u_1} [semiring R] :
@[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_right_inverse {n : } {R : Type u_1} [ring R] (f : R →+* zmod n) :
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 : f.ker = g.ker) :
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}) :