Documentation

Init.Data.Fin.Basic

instance Fin.coeToNat {n : Nat} :
Coe (Fin n) Nat
Equations
  • Fin.coeToNat = { coe := fun v => v.val }
def Fin.elim0 {α : Sort u} :
Fin 0α
Equations
  • Fin.elim0 _fun_discr = match _fun_discr with | { val := val, isLt := h } => absurd h (_ : ¬val < 0)
def Fin.succ {n : Nat} :
Fin nFin (Nat.succ n)
Equations
def Fin.ofNat {n : Nat} (a : Nat) :
Equations
def Fin.ofNat' {n : Nat} (a : Nat) (h : n > 0) :
Fin n
Equations
def Fin.add {n : Nat} :
Fin nFin nFin n
Equations
  • Fin.add _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := (a + b) % n, isLt := (_ : (a + b) % n < n) }
def Fin.mul {n : Nat} :
Fin nFin nFin n
Equations
  • Fin.mul _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a * b % n, isLt := (_ : a * b % n < n) }
def Fin.sub {n : Nat} :
Fin nFin nFin n
Equations
  • Fin.sub _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := (a + (n - b)) % n, isLt := (_ : (a + (n - b)) % n < n) }
def Fin.mod {n : Nat} :
Fin nFin nFin n
Equations
  • Fin.mod _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a % b % n, isLt := (_ : a % b % n < n) }
def Fin.div {n : Nat} :
Fin nFin nFin n
Equations
  • Fin.div _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a / b % n, isLt := (_ : a / b % n < n) }
def Fin.modn {n : Nat} :
Fin nNatFin n
Equations
  • Fin.modn _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { val := a, isLt := h }, m => { val := a % m % n, isLt := (_ : a % m % n < n) }
def Fin.land {n : Nat} :
Fin nFin nFin n
Equations
  • Fin.land _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := Nat.land a b % n, isLt := (_ : Nat.land a b % n < n) }
def Fin.lor {n : Nat} :
Fin nFin nFin n
Equations
  • Fin.lor _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := Nat.lor a b % n, isLt := (_ : Nat.lor a b % n < n) }
def Fin.xor {n : Nat} :
Fin nFin nFin n
Equations
  • Fin.xor _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := Nat.xor a b % n, isLt := (_ : Nat.xor a b % n < n) }
def Fin.shiftLeft {n : Nat} :
Fin nFin nFin n
Equations
  • Fin.shiftLeft _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a <<< b % n, isLt := (_ : a <<< b % n < n) }
def Fin.shiftRight {n : Nat} :
Fin nFin nFin n
Equations
  • Fin.shiftRight _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a >>> b % n, isLt := (_ : a >>> b % n < n) }
instance Fin.instAddFin {n : Nat} :
Add (Fin n)
Equations
  • Fin.instAddFin = { add := Fin.add }
instance Fin.instSubFin {n : Nat} :
Sub (Fin n)
Equations
  • Fin.instSubFin = { sub := Fin.sub }
instance Fin.instMulFin {n : Nat} :
Mul (Fin n)
Equations
  • Fin.instMulFin = { mul := Fin.mul }
instance Fin.instModFin {n : Nat} :
Mod (Fin n)
Equations
  • Fin.instModFin = { mod := Fin.mod }
instance Fin.instDivFin {n : Nat} :
Div (Fin n)
Equations
  • Fin.instDivFin = { div := Fin.div }
instance Fin.instAndOpFin {n : Nat} :
Equations
  • Fin.instAndOpFin = { and := Fin.land }
instance Fin.instOrOpFin {n : Nat} :
OrOp (Fin n)
Equations
  • Fin.instOrOpFin = { or := Fin.lor }
instance Fin.instXorFin {n : Nat} :
Xor (Fin n)
Equations
  • Fin.instXorFin = { xor := Fin.xor }
instance Fin.instShiftLeftFin {n : Nat} :
Equations
  • Fin.instShiftLeftFin = { shiftLeft := Fin.shiftLeft }
instance Fin.instShiftRightFin {n : Nat} :
Equations
  • Fin.instShiftRightFin = { shiftRight := Fin.shiftRight }
instance Fin.instHModFinNat {n : Nat} :
HMod (Fin n) Nat (Fin n)
Equations
  • Fin.instHModFinNat = { hMod := Fin.modn }
Equations
  • Fin.instOfNatFinHAddNatInstHAddInstAddNatOfNat = { ofNat := Fin.ofNat i }
Equations
  • Fin.instInhabitedFinHAddNatInstHAddInstAddNatOfNat = { default := 0 }
theorem Fin.val_ne_of_ne {n : Nat} {i : Fin n} {j : Fin n} (h : i j) :
i.val j.val
theorem Fin.modn_lt {n : Nat} {m : Nat} (i : Fin n) :
m > 0(i % m).val < m