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.

def fin.has_neg (n : ) :

Negation on fin n

Equations

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

Equations
def fin.comm_semigroup (n : ) :

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

Equations
def fin.comm_ring (n : ) :
comm_ring (fin (n + 1))

Commutative ring 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

theorem zmod.val_cast_nat {n : } (a : ) :
a.val = a % n

@[instance]
def zmod.char_p (n : ) :
char_p (zmod n) n

@[simp]
theorem zmod.cast_self (n : ) :
n = 0

@[simp]
theorem zmod.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.cast_val {n : } [fact (0 < n)] (a : zmod n) :
(a.val) = a

@[simp]
theorem zmod.cast_id (n : ) (i : zmod n) :
i = i

@[simp]
theorem zmod.nat_cast_val {n : } {R : Type u_1} [ring R] [fact (0 < n)] (i : zmod n) :
(i.val) = i

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] :
m n1 = 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.

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] :

def zmod.ring_equiv {n : } (R : Type u_1) [ring R] [char_p R n] [fintype R] :
fintype.card R = nzmod n ≃+* R

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.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.cast_mod_int (a : ) (b : ) :
(a % b) = a

@[simp]
theorem zmod.coe_to_nat (p : ) {z : } :
0 z(z.to_nat) = 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.cast_mod_nat (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 : ) :
x.coprime n(x) * (x)⁻¹ = 1

def zmod.unit_of_coprime {n : } (x : ) :
x.coprime nunits (zmod 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.cast_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) :
is_unit aa * a⁻¹ = 1

theorem zmod.inv_mul_of_unit {n : } (a : zmod n) :
is_unit aa⁻¹ * 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} :
x 0(x.val n / 2 n / 2 < (-x).val)

theorem zmod.ne_neg_self (n : ) [hn : fact (n % 2 = 1)] {a : zmod n} :
a 0a -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 : } :
a < na.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.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)] :
p qq 0

@[instance]
def zmod.field (p : ) [fact (nat.prime p)] :

Field structure on zmod p if p is prime.

Equations
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] :

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) :
f.ker = g.kerf = g