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

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

def fin.has_neg (n : ℕ) :

has_neg (fin n)

Negation on fin n

Equations

fin.has_neg n = {neg := λ (a : fin n), ⟨(-↑(a.val)).nat_mod ↑n, _⟩}

source

def fin.add_comm_semigroup (n : ℕ) :

add_comm_semigroup (fin (n + 1))

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

Equations

fin.add_comm_semigroup n = {add := has_add.add fin.has_add, add_assoc := _, add_comm := _}

source

def fin.comm_semigroup (n : ℕ) :

comm_semigroup (fin (n + 1))

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

Equations

fin.comm_semigroup n = {mul := has_mul.mul fin.has_mul, mul_assoc := _, mul_comm := _}

source

def fin.comm_ring (n : ℕ) :

comm_ring (fin (n + 1))

Commutative ring structure on fin (n+1).

Equations

fin.comm_ring n = {add := add_comm_semigroup.add (fin.add_comm_semigroup n), add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := has_neg.neg (fin.has_neg (n + 1)), add_left_neg := _, add_comm := _, mul := comm_semigroup.mul (fin.comm_semigroup n), mul_assoc := _, one := 1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

def zmod :

ℕ → Type

The integers modulo n : ℕ.

Equations

zmod (n + 1) = fin (n + 1)
zmod 0 = ℤ

source

@[instance]

def zmod.fintype (n : ℕ) [fact (0 < n)] :

fintype (zmod n)

Equations

zmod.fintype (n + 1) = fin.fintype (n + 1)
zmod.fintype 0 = _.elim

source

theorem zmod.card (n : ℕ) [fact (0 < n)] :

fintype.card (zmod n) = n

source

@[instance]

def zmod.decidable_eq (n : ℕ) :

decidable_eq (zmod n)

Equations

zmod.decidable_eq (n + 1) = fin.decidable_eq (n.add 0 + 1)
zmod.decidable_eq 0 = int.decidable_eq

source

@[instance]

def zmod.has_repr (n : ℕ) :

has_repr (zmod n)

Equations

zmod.has_repr (n + 1) = fin.has_repr (n.add 0 + 1)
zmod.has_repr 0 = int.has_repr

source

@[instance]

def zmod.comm_ring (n : ℕ) :

comm_ring (zmod n)

Equations

zmod.comm_ring (n + 1) = fin.comm_ring n
zmod.comm_ring 0 = int.comm_ring

source

@[instance]

def zmod.inhabited (n : ℕ) :

inhabited (zmod n)

Equations

zmod.inhabited n = {default := 0}

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

@[simp]

theorem zmod.val_zero {n : ℕ} :

0.val = 0

source

theorem zmod.val_cast_nat {n : ℕ} (a : ℕ) :

↑a.val = a % n

source

@[instance]

def zmod.char_p (n : ℕ) :

char_p (zmod n) n

Equations

_ = _

source

@[simp]

theorem zmod.cast_self (n : ℕ) :

↑n = 0

source

@[simp]

theorem zmod.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

zmod.cast = λ (i : zmod (n + 1)), ↑(i.val)
zmod.cast = int.cast

source

@[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

zmod.has_coe_t n = {coe := zmod.cast n}

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

theorem zmod.nat_cast_surjective {n : ℕ} [fact (0 < n)] :

function.surjective coe

source

theorem zmod.int_cast_surjective {n : ℕ} :

function.surjective coe

source

theorem zmod.cast_val {n : ℕ} [fact (0 < n)] (a : zmod n) :

↑(a.val) = a

source

@[simp]

theorem zmod.cast_id (n : ℕ) (i : zmod n) :

↑i = i

source

@[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.

source

@[simp]

theorem zmod.cast_one {n : ℕ} {R : Type u_1} [ring R] {m : ℕ} [char_p R m] :

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.

Equations

zmod.cast_hom h R = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

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

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

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

theorem zmod.cast_nat_cast {n : ℕ} {R : Type u_1} [ring R] {m : ℕ} [char_p R m] (h : m ∣ n) (k : ℕ) :

↑↑k = ↑k

source

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]

theorem zmod.cast_nat_cast' {n : ℕ} {R : Type u_1} [ring R] [char_p R n] (k : ℕ) :

↑↑k = ↑k

source

@[simp]

theorem zmod.cast_int_cast' {n : ℕ} {R : Type u_1} [ring R] [char_p R n] (k : ℤ) :

↑↑k = ↑k

source

theorem zmod.int_coe_eq_int_coe_iff (a b : ℤ) (c : ℕ) :

↑a = ↑b ↔ a ≡ b [ZMOD ↑c]

source

theorem zmod.nat_coe_eq_nat_coe_iff (a b c : ℕ) :

↑a = ↑b ↔ a ≡ b [MOD c]

source

theorem zmod.int_coe_zmod_eq_zero_iff_dvd (a : ℤ) (b : ℕ) :

↑a = 0 ↔ ↑b ∣ a

source

theorem zmod.nat_coe_zmod_eq_zero_iff_dvd (a b : ℕ) :

↑a = 0 ↔ b ∣ a

source

theorem zmod.cast_mod_int (a : ℤ) (b : ℕ) :

↑(a % ↑b) = ↑a

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

@[instance]

def zmod.nontrivial (n : ℕ) [fact (1 < n)] :

nontrivial (zmod n)

Equations

_ = _

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