mathlib3 documentation

core / init.data.fin.ops

@[protected]

def fin.succ {n : ℕ} :

fin n → fin n.succ

Equations

⟨a, h⟩.succ = ⟨a.succ, _⟩

def fin.of_nat {n : ℕ} (a : ℕ) :

Equations

fin.of_nat a = ⟨a % n.succ, _⟩

@[protected]

def fin.add {n : ℕ} :

fin n → fin n → fin n

Equations

⟨a, h⟩.add ⟨b, _x⟩ = ⟨(a + b) % n, _⟩

@[protected]

def fin.mul {n : ℕ} :

fin n → fin n → fin n

Equations

⟨a, h⟩.mul ⟨b, _x⟩ = ⟨a * b % n, _⟩

@[protected]

def fin.sub {n : ℕ} :

fin n → fin n → fin n

Equations

⟨a, h⟩.sub ⟨b, _x⟩ = ⟨(a + (n - b)) % n, _⟩

@[protected]

def fin.mod {n : ℕ} :

fin n → fin n → fin n

Equations

⟨a, h₁⟩.mod ⟨b, h₂⟩ = ⟨a % b, _⟩

@[protected]

def fin.div {n : ℕ} :

fin n → fin n → fin n

Equations

⟨a, h⟩.div ⟨b, _x⟩ = ⟨a / b, _⟩

@[protected, instance]

def fin.has_zero {n : ℕ} :

has_zero (fin n.succ)

Equations

fin.has_zero = {zero := ⟨0, _⟩}

@[protected, instance]

def fin.has_one {n : ℕ} :

has_one (fin n.succ)

Equations

fin.has_one = {one := fin.of_nat 1}

@[protected, instance]

def fin.has_add {n : ℕ} :

has_add (fin n)

Equations

fin.has_add = {add := fin.add n}

@[protected, instance]

def fin.has_sub {n : ℕ} :

has_sub (fin n)

Equations

fin.has_sub = {sub := fin.sub n}

@[protected, instance]

def fin.has_mul {n : ℕ} :

has_mul (fin n)

Equations

fin.has_mul = {mul := fin.mul n}

@[protected, instance]

def fin.has_mod {n : ℕ} :

has_mod (fin n)

Equations

fin.has_mod = {mod := fin.mod n}

@[protected, instance]

def fin.has_div {n : ℕ} :

has_div (fin n)

Equations

fin.has_div = {div := fin.div n}

theorem fin.of_nat_zero {n : ℕ} :

fin.of_nat 0 = 0

theorem fin.add_def {n : ℕ} (a b : fin n) :

(a + b).val = (a.val + b.val) % n

theorem fin.mul_def {n : ℕ} (a b : fin n) :

(a * b).val = a.val * b.val % n

theorem fin.sub_def {n : ℕ} (a b : fin n) :

(a - b).val = (a.val + (n - b.val)) % n

theorem fin.mod_def {n : ℕ} (a b : fin n) :

(a % b).val = a.val % b.val

theorem fin.div_def {n : ℕ} (a b : fin n) :

(a / b).val = a.val / b.val

theorem fin.lt_def {n : ℕ} (a b : fin n) :

a < b = (a.val < b.val)

theorem fin.le_def {n : ℕ} (a b : fin n) :

a ≤ b = (a.val ≤ b.val)

@[simp]

theorem fin.val_zero {n : ℕ} :

0.val = 0

def fin.pred {n : ℕ} (i : fin n.succ) :

i ≠ 0 → fin n

Equations

⟨a, h₁⟩.pred h₂ = ⟨a.pred, _⟩