mathlib documentation

core / init.data.fin.ops

def fin.succ {n : } :
fin nfin n.succ
Equations
def fin.of_nat {n : } (a : ) :
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 + (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 0fin n
Equations