mathlib documentation

core.init.data.fin.ops

def fin.succ {n : } :
fin nfin n.succ

Equations
def fin.of_nat {n : } :
fin n.succ

Equations
def fin.add {n : } :
fin nfin nfin n

Equations
def fin.mul {n : } :
fin nfin nfin n

Equations
def fin.sub {n : } :
fin nfin nfin n

Equations
def fin.mod {n : } :
fin nfin nfin n

Equations
def fin.div {n : } :
fin nfin nfin n

Equations
@[instance]
def fin.has_zero {n : } :

Equations
@[instance]
def fin.has_one {n : } :

Equations
@[instance]
def fin.has_add {n : } :

Equations
@[instance]
def fin.has_sub {n : } :

Equations
@[instance]
def fin.has_mul {n : } :

Equations
@[instance]
def fin.has_mod {n : } :

Equations
@[instance]
def fin.has_div {n : } :

Equations
theorem fin.of_nat_zero {n : } :

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 - b.val

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 0fin n

Equations