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.

source
@[protected, instance]
def fin.comm_semigroup (n : ℕ) :
comm_semigroup (fin (n + 1))

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

Equations
source
@[protected, instance]
def fin.comm_ring (n : ℕ) :
comm_ring (fin (n + 1))

Commutative ring structure on fin (n+1).

Equations
source
def zmod  :
ℕ → Type

The integers modulo n : ℕ.

Equations
source
@[protected, instance]
def zmod.fintype (n : ℕ) [fact (0 < n)] :
fintype (zmod n)
Equations
source
@[simp]
theorem zmod.card (n : ℕ) [fact (0 < n)] :
fintype.card (zmod n) = n
source
@[protected, instance]
def zmod.decidable_eq (n : ℕ) :
decidable_eq (zmod n)
Equations
source
@[protected, instance]
def zmod.has_repr (n : ℕ) :
has_repr (zmod n)
Equations
source
@[protected, instance]
def zmod.comm_ring (n : ℕ) :
comm_ring (zmod n)
Equations
source
@[protected, instance]
def zmod.inhabited (n : ℕ) :
inhabited (zmod n)
Equations
source
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
source
theorem zmod.val_lt {n : ℕ} [fact (0 < n)] (a : zmod n) :
a.val < n
source
theorem zmod.val_le {n : ℕ} [fact (0 < n)] (a : zmod n) :
a.val ≤ n
source
@[simp]
theorem zmod.val_zero {n : ℕ} :
0.val = 0
source
@[simp]
theorem zmod.val_one'  :
1.val = 1
source
@[simp]
theorem zmod.val_neg' {n : zmod 0} :
(-n).val = n.val
source
@[simp]
theorem zmod.val_mul' {m n : zmod 0} :
(m * n).val = (m.val) * n.val
source
theorem zmod.val_nat_cast {n : ℕ} (a : ℕ) :
↑a.val = a % n
source
@[protected, instance]
def zmod.char_p (n : ℕ) :
char_p (zmod n) n
source
@[simp]
theorem zmod.nat_cast_self (n : ℕ) :
↑n = 0
source
@[simp]
theorem zmod.nat_cast_self' (n : ℕ) :
↑n + 1 = 0
source
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
source
@[protected, instance]
def zmod.has_coe_t {R : Type u_1} [has_zero R] [has_one R] [has_add R] [has_neg R] (n : ℕ) :
has_coe_t (zmod n) R
Equations
source
@[simp]
theorem zmod.cast_zero {n : ℕ} {R : Type u_1} [has_zero R] [has_one R] [has_add R] [has_neg R] :
↑0 = 0
source
@[simp]
theorem prod.fst_zmod_cast {n : ℕ} {R : Type u_1} [has_zero R] [has_one R] [has_add R] [has_neg R] {S : Type u_2} [has_zero S] [has_one S] [has_add S] [has_neg S] (a : zmod n) :
↑a.fst = ↑a
source
@[simp]
theorem prod.snd_zmod_cast {n : ℕ} {R : Type u_1} [has_zero R] [has_one R] [has_add R] [has_neg R] {S : Type u_2} [has_zero S] [has_one S] [has_add S] [has_neg S] (a : zmod n) :
↑a.snd = ↑a
source
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.

source
theorem zmod.nat_cast_right_inverse {n : ℕ} [fact (0 < n)] :
function.right_inverse zmod.val coe
source
theorem zmod.nat_cast_zmod_surjective {n : ℕ} [fact (0 < n)] :
function.surjective coe
source
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.

source
theorem zmod.int_cast_right_inverse {n : ℕ} :
function.right_inverse coe coe
source
theorem zmod.int_cast_surjective {n : ℕ} :
function.surjective coe
source
@[norm_cast]
theorem zmod.cast_id (n : ℕ) (i : zmod n) :
↑i = i
source
@[simp]
theorem zmod.cast_id' {n : ℕ} :
coe = id
source
@[simp]
theorem zmod.nat_cast_comp_val {n : ℕ} (R : Type u_1) [ring R] [fact (0 < n)] :
coe ∘ zmod.val = coe

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

source
@[simp]
theorem zmod.int_cast_comp_cast {n : ℕ} (R : Type u_1) [ring R] :
coe ∘ coe = coe

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

source
@[simp]
theorem zmod.nat_cast_val {n : ℕ} {R : Type u_1} [ring R] [fact (0 < n)] (i : zmod n) :
↑(i.val) = ↑i
source
@[simp]
theorem zmod.int_cast_cast {n : ℕ} {R : Type u_1} [ring R] (i : zmod n) :
↑↑i = ↑i
source
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.

source
@[simp]
theorem zmod.cast_one {n : ℕ} {R : Type u_1} [ring R] {m : ℕ} [char_p R m] (h : m ∣ n) :
↑1 = 1
source
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
source
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
source
def zmod.cast_hom {n m : ℕ} (h : m ∣ n) (R : Type u_1) [ring R] [char_p R m] :
zmod n →+* R

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
source
@[simp]
theorem zmod.cast_hom_apply {n : ℕ} {R : Type u_1} [ring R] {m : ℕ} [char_p R m] {h : m ∣ n} (i : zmod n) :
⇑(zmod.cast_hom h R) i = ↑i
source
@[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
source
@[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) :
↑-a = -↑a
source
@[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
source
@[simp, norm_cast]
theorem zmod.cast_nat_cast {n : ℕ} {R : Type u_1} [ring R] {m : ℕ} [char_p R m] (h : m ∣ n) (k : ℕ) :
↑↑k = ↑k
source
@[simp, norm_cast]
theorem zmod.cast_int_cast {n : ℕ} {R : Type u_1} [ring R] {m : ℕ} [char_p R m] (h : m ∣ n) (k : ℤ) :
↑↑k = ↑k

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

source
@[simp]
theorem zmod.cast_one' {n : ℕ} {R : Type u_1} [ring R] [char_p R n] :
↑1 = 1
source
@[simp]
theorem zmod.cast_add' {n : ℕ} {R : Type u_1} [ring R] [char_p R n] (a b : zmod n) :
↑(a + b) = ↑a + ↑b
source
@[simp]
theorem zmod.cast_mul' {n : ℕ} {R : Type u_1} [ring R] [char_p R n] (a b : zmod n) :
↑a * b = (↑a) * ↑b
source
@[simp]
theorem zmod.cast_sub' {n : ℕ} {R : Type u_1} [ring R] [char_p R n] (a b : zmod n) :
↑(a - b) = ↑a - ↑b
source
@[simp]
theorem zmod.cast_pow' {n : ℕ} {R : Type u_1} [ring R] [char_p R n] (a : zmod n) (k : ℕ) :
↑(a ^ k) = ↑a ^ k
source
@[simp, norm_cast]
theorem zmod.cast_nat_cast' {n : ℕ} {R : Type u_1} [ring R] [char_p R n] (k : ℕ) :
↑↑k = ↑k
source
@[simp, norm_cast]
theorem zmod.cast_int_cast' {n : ℕ} {R : Type u_1} [ring R] [char_p R n] (k : ℤ) :
↑↑k = ↑k
source
theorem zmod.cast_hom_injective {n : ℕ} (R : Type u_1) [ring R] [char_p R n] :
function.injective ⇑(zmod.cast_hom _ R)
source
theorem zmod.cast_hom_bijective {n : ℕ} (R : Type u_1) [ring R] [char_p R n] [fintype R] (h : fintype.card R = n) :
function.bijective ⇑(zmod.cast_hom _ R)
source
noncomputable def zmod.ring_equiv {n : ℕ} (R : Type u_1) [ring R] [char_p R n] [fintype R] (h : fintype.card R = n) :
zmod n ≃+* R

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

Equations
source
theorem zmod.int_coe_eq_int_coe_iff (a b : ℤ) (c : ℕ) :
↑a = ↑b ↔ a ≡ b [ZMOD ↑c]
source
theorem zmod.int_coe_eq_int_coe_iff' (a b : ℤ) (c : ℕ) :
↑a = ↑b ↔ a % ↑c = b % ↑c
source
theorem zmod.nat_coe_eq_nat_coe_iff (a b c : ℕ) :
↑a = ↑b ↔ a ≡ b [MOD c]
source
theorem zmod.nat_coe_eq_nat_coe_iff' (a b c : ℕ) :
↑a = ↑b ↔ a % c = b % c
source
theorem zmod.int_coe_zmod_eq_zero_iff_dvd (a : ℤ) (b : ℕ) :
↑a = 0 ↔ ↑b ∣ a
source
theorem zmod.int_coe_eq_int_coe_iff_dvd_sub (a b : ℤ) (c : ℕ) :
↑a = ↑b ↔ ↑c ∣ b - a
source
theorem zmod.nat_coe_zmod_eq_zero_iff_dvd (a b : ℕ) :
↑a = 0 ↔ b ∣ a
source
theorem zmod.val_int_cast {n : ℕ} (a : ℤ) [fact (0 < n)] :
↑(↑a.val) = a % ↑n
source
theorem zmod.nat_coe_zmod_eq_iff (p n : ℕ) (z : zmod p) [fact (0 < p)] :
↑n = z ↔ ∃ (k : ℕ), n = z.val + p * k
source
theorem zmod.int_coe_zmod_eq_iff (p : ℕ) (n : ℤ) (z : zmod p) [fact (0 < p)] :
↑n = z ↔ ∃ (k : ℤ), n = ↑(z.val) + (↑p) * k
source
@[simp]
theorem zmod.int_cast_mod (a : ℤ) (b : ℕ) :
↑(a % ↑b) = ↑a
source
theorem zmod.ker_int_cast_add_hom (n : ℕ) :
(int.cast_add_hom (zmod n)).ker = add_subgroup.zmultiples ↑n
source
theorem zmod.ker_int_cast_ring_hom (n : ℕ) :
(int.cast_ring_hom (zmod n)).ker = ideal.span {↑n}
source
@[simp]
theorem zmod.nat_cast_to_nat (p : ℕ) {z : ℤ} (h : 0 ≤ z) :
↑(z.to_nat) = ↑z
source
theorem zmod.val_injective (n : ℕ) [fact (0 < n)] :
function.injective zmod.val
source
theorem zmod.val_one_eq_one_mod (n : ℕ) :
1.val = 1 % n
source
theorem zmod.val_one (n : ℕ) [fact (1 < n)] :
1.val = 1
source
theorem zmod.val_add {n : ℕ} [fact (0 < n)] (a b : zmod n) :
(a + b).val = (a.val + b.val) % n
source
theorem zmod.val_mul {n : ℕ} (a b : zmod n) :
(a * b).val = (a.val) * b.val % n
source
@[protected, instance]
def zmod.nontrivial (n : ℕ) [fact (1 < n)] :
nontrivial (zmod n)
source
def zmod.inv (n : ℕ) :
zmod n → zmod 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
source
@[protected, instance]
def zmod.has_inv (n : ℕ) :
has_inv (zmod n)
Equations
source
theorem zmod.inv_zero (n : ℕ) :
0⁻¹ = 0
source
theorem zmod.mul_inv_eq_gcd {n : ℕ} (a : zmod n) :
a * a⁻¹ = ↑(a.val.gcd n)
source
@[simp]
theorem zmod.nat_cast_mod (n a : ℕ) :
↑(a % n) = ↑a
source
theorem zmod.eq_iff_modeq_nat (n : ℕ) {a b : ℕ} :
↑a = ↑b ↔ a ≡ b [MOD n]
source
theorem zmod.coe_mul_inv_eq_one {n : ℕ} (x : ℕ) (h : x.coprime n) :
(↑x) * (↑x)⁻¹ = 1
source
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
source
@[simp]
theorem zmod.coe_unit_of_coprime {n : ℕ} (x : ℕ) (h : x.coprime n) :
↑(zmod.unit_of_coprime x h) = ↑x
source
theorem zmod.val_coe_unit_coprime {n : ℕ} (u : (zmod n)ˣ) :
↑u.val.coprime n
source
@[simp]
theorem zmod.inv_coe_unit {n : ℕ} (u : (zmod n)ˣ) :
(↑u)⁻¹ = ↑u⁻¹
source
theorem zmod.mul_inv_of_unit {n : ℕ} (a : zmod n) (h : is_unit a) :
a * a⁻¹ = 1
source
theorem zmod.inv_mul_of_unit {n : ℕ} (a : zmod n) (h : is_unit a) :
a⁻¹ * a = 1
source
def zmod.units_equiv_coprime {n : ℕ} [fact (0 < 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
source
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
source
@[protected, instance]
def zmod.subsingleton_units  :
subsingleton (zmod 2)ˣ
source
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
source
theorem zmod.ne_neg_self (n : ℕ) [hn : fact (n % 2 = 1)] {a : zmod n} (ha : a ≠ 0) :
a ≠ -a
source
theorem zmod.neg_one_ne_one {n : ℕ} [fact (2 < n)] :
-1 ≠ 1
source
theorem zmod.neg_eq_self_mod_two (a : zmod 2) :
-a = a
source
@[simp]
theorem zmod.nat_abs_mod_two (a : ℤ) :
↑(a.nat_abs) = ↑a
source
@[simp]
theorem zmod.val_eq_zero {n : ℕ} (a : zmod n) :
a.val = 0 ↔ a = 0
source
theorem zmod.val_cast_of_lt {n a : ℕ} (h : a < n) :
↑a.val = a
source
theorem zmod.neg_val' {n : ℕ} [fact (0 < n)] (a : zmod n) :
(-a).val = (n - a.val) % n
source
theorem zmod.neg_val {n : ℕ} [fact (0 < n)] (a : zmod n) :
(-a).val = ite (a = 0) 0 (n - a.val)
source
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
source
@[simp]
theorem zmod.val_min_abs_def_zero (x : zmod 0) :
x.val_min_abs = x
source
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)
source
@[simp]
theorem zmod.coe_val_min_abs {n : ℕ} (x : zmod n) :
↑(x.val_min_abs) = x
source
theorem zmod.nat_abs_val_min_abs_le {n : ℕ} [fact (0 < n)] (x : zmod n) :
x.val_min_abs.nat_abs ≤ n / 2
source
@[simp]
theorem zmod.val_min_abs_zero (n : ℕ) :
0.val_min_abs = 0
source
@[simp]
theorem zmod.val_min_abs_eq_zero {n : ℕ} (x : zmod n) :
x.val_min_abs = 0 ↔ x = 0
source
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)
source
@[simp]
theorem zmod.nat_abs_val_min_abs_neg {n : ℕ} (a : zmod n) :
(-a).val_min_abs.nat_abs = a.val_min_abs.nat_abs
source
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
source
theorem zmod.prime_ne_zero (p q : ℕ) [hp : fact (nat.prime p)] [hq : fact (nat.prime q)] (hpq : p ≠ q) :
↑q ≠ 0
source
@[protected, instance]
def zmod.field (p : ℕ) [fact (nat.prime p)] :
field (zmod p)

Field structure on zmod p if p is prime.

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

zmod p is an integral domain when p is prime.

source
theorem ring_hom.ext_zmod {n : ℕ} {R : Type u_1} [semiring R] (f g : zmod n →+* R) :
f = g
source
@[protected, instance]
def zmod.subsingleton_ring_hom {n : ℕ} {R : Type u_1} [semiring R] :
subsingleton (zmod n →+* R)
source
@[protected, instance]
def zmod.subsingleton_ring_equiv {n : ℕ} {R : Type u_1} [semiring R] :
subsingleton (zmod n ≃+* R)
source
@[simp]
theorem zmod.ring_hom_map_cast {n : ℕ} {R : Type u_1} [ring R] (f : R →+* zmod n) (k : zmod n) :
⇑f ↑k = k
source
theorem zmod.ring_hom_right_inverse {n : ℕ} {R : Type u_1} [ring R] (f : R →+* zmod n) :
function.right_inverse coe ⇑f
source
theorem zmod.ring_hom_surjective {n : ℕ} {R : Type u_1} [ring R] (f : R →+* zmod n) :
function.surjective ⇑f
source
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
source
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
source
@[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
source
@[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
source
@[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
source
theorem zmod.lift_cast_add_hom (n : ℕ) {A : Type u_2} [add_group A] (f : {f // ⇑f ↑n = 0}) (x : ℤ) :
⇑(⇑(zmod.lift n) f) (⇑(int.cast_add_hom (zmod n)) x) = ⇑f x
source
@[simp]
theorem zmod.lift_comp_coe (n : ℕ) {A : Type u_2} [add_group A] (f : {f // ⇑f ↑n = 0}) :
⇑(⇑(zmod.lift n) f) ∘ coe = ⇑f
source
@[simp]
theorem zmod.lift_comp_cast_add_hom (n : ℕ) {A : Type u_2} [add_group A] (f : {f // ⇑f ↑n = 0}) :
(⇑(zmod.lift n) f).comp (int.cast_add_hom (zmod n)) = ↑f