# Documentation

## Init.Data.Fin.Basic

instance Fin.coeToNat {n : Nat} :
Equations
• Fin.coeToNat = { coe := fun (v : Fin n) => v }
def Fin.elim0 {α : Sort u} :
Fin 0α
Equations
• = match x with | { val := val, isLt := h } => absurd h
Instances For
def Fin.succ {n : Nat} :
Fin nFin ()
Equations
• = match x with | { val := i, isLt := h } => { val := i + 1, isLt := }
Instances For
def Fin.ofNat {n : Nat} (a : Nat) :
Fin ()
Equations
• = { val := a % (n + 1), isLt := }
Instances For
def Fin.ofNat' {n : Nat} (a : Nat) (h : n > 0) :
Fin n
Equations
• = { val := a % n, isLt := }
Instances For
def Fin.add {n : Nat} :
Fin nFin nFin n
Equations
• Fin.add x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := (a + b) % n, isLt := }
Instances For
def Fin.mul {n : Nat} :
Fin nFin nFin n
Equations
• Fin.mul x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a * b % n, isLt := }
Instances For
def Fin.sub {n : Nat} :
Fin nFin nFin n
Equations
• Fin.sub x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := (a + (n - b)) % n, isLt := }
Instances For

Remark: land/lor can be defined without using (% n), but we are trying to minimize the number of Nat theorems needed to bootstrap Lean.

def Fin.mod {n : Nat} :
Fin nFin nFin n
Equations
• Fin.mod x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a % b, isLt := }
Instances For
def Fin.div {n : Nat} :
Fin nFin nFin n
Equations
• Fin.div x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a / b, isLt := }
Instances For
def Fin.modn {n : Nat} :
Fin nNatFin n
Equations
• Fin.modn x✝ x = match x✝, x with | { val := a, isLt := h }, m => { val := a % m, isLt := }
Instances For
def Fin.land {n : Nat} :
Fin nFin nFin n
Equations
• Fin.land x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := Nat.land a b % n, isLt := }
Instances For
def Fin.lor {n : Nat} :
Fin nFin nFin n
Equations
• Fin.lor x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := Nat.lor a b % n, isLt := }
Instances For
def Fin.xor {n : Nat} :
Fin nFin nFin n
Equations
• Fin.xor x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := Nat.xor a b % n, isLt := }
Instances For
def Fin.shiftLeft {n : Nat} :
Fin nFin nFin n
Equations
• = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a <<< b % n, isLt := }
Instances For
def Fin.shiftRight {n : Nat} :
Fin nFin nFin n
Equations
• = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a >>> b % n, isLt := }
Instances For
instance Fin.instAddFin {n : Nat} :
Equations
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 }
Equations
• Fin.instShiftLeftFin = { shiftLeft := Fin.shiftLeft }
Equations
• Fin.instShiftRightFin = { shiftRight := Fin.shiftRight }
instance Fin.instOfNat {n : Nat} {i : Nat} :
OfNat (Fin (n + 1)) i
Equations
• Fin.instOfNat = { ofNat := }
Equations
@[simp]
theorem Fin.zero_eta {n : Nat} :
{ val := 0, isLt := } = 0
theorem Fin.val_ne_of_ne {n : Nat} {i : Fin n} {j : Fin n} (h : i j) :
i j
theorem Fin.modn_lt {n : Nat} {m : Nat} (i : Fin n) :
m > 0(Fin.modn i m) < m
theorem Fin.val_lt_of_le {n : Nat} {b : Nat} (i : Fin b) (h : b n) :
i < n
theorem Fin.pos {n : Nat} (i : Fin n) :
0 < n
@[inline]
def Fin.last (n : Nat) :
Fin (n + 1)

The greatest value of Fin (n+1).

Equations
• = { val := n, isLt := }
Instances For
@[inline]
def Fin.castLT {n : Nat} {m : Nat} (i : Fin m) (h : i < n) :
Fin n

castLT i h embeds i into a Fin where h proves it belongs into.

Equations
• = { val := i, isLt := h }
Instances For
@[inline]
def Fin.castLE {n : Nat} {m : Nat} (h : n m) (i : Fin n) :
Fin m

castLE h i embeds i into a larger Fin type.

Equations
• = { val := i, isLt := }
Instances For
@[inline]
def Fin.cast {n : Nat} {m : Nat} (eq : n = m) (i : Fin n) :
Fin m

cast eq i embeds i into an equal Fin type.

Equations
Instances For
@[inline]
def Fin.castAdd {n : Nat} (m : Nat) :
Fin nFin (n + m)

Equations
Instances For
@[inline]
def Fin.castSucc {n : Nat} :
Fin nFin (n + 1)

castSucc i embeds i : Fin n in Fin (n+1).

Equations
• Fin.castSucc =
Instances For
def Fin.addNat {n : Nat} (i : Fin n) (m : Nat) :
Fin (n + m)

addNat m i adds m to i, generalizes Fin.succ.

Equations
• = { val := i + m, isLt := }
Instances For
def Fin.natAdd {m : Nat} (n : Nat) (i : Fin m) :
Fin (n + m)

natAdd n i adds n to i "on the left".

Equations
• = { val := n + i, isLt := }
Instances For
@[inline]
def Fin.rev {n : Nat} (i : Fin n) :
Fin n

Maps 0 to n-1, 1 to n-2, ..., n-1 to 0.

Equations
• = { val := n - (i + 1), isLt := }
Instances For
@[inline]
def Fin.subNat {n : Nat} (m : Nat) (i : Fin (n + m)) (h : m i) :
Fin n

subNat i h subtracts m from i, generalizes Fin.pred.

Equations
Instances For
@[inline]
def Fin.pred {n : Nat} (i : Fin (n + 1)) (h : i 0) :
Fin n

Predecessor of a nonzero element of Fin (n+1).

Equations
Instances For
theorem Fin.val_inj {n : Nat} {a : Fin n} {b : Fin n} :
a = b a = b
theorem Fin.val_congr {n : Nat} {a : Fin n} {b : Fin n} (h : a = b) :
a = b
theorem Fin.val_le_of_le {n : Nat} {a : Fin n} {b : Fin n} (h : a b) :
a b
theorem Fin.val_le_of_ge {n : Nat} {a : Fin n} {b : Fin n} (h : a b) :
b a
theorem Fin.val_add_one_le_of_lt {n : Nat} {a : Fin n} {b : Fin n} (h : a < b) :
a + 1 b
theorem Fin.val_add_one_le_of_gt {n : Nat} {a : Fin n} {b : Fin n} (h : a > b) :
b + 1 a
instance instGetElemFinVal {cont : Type u_1} {elem : Type u_2} {dom : cont} {n : Nat} [GetElem cont Nat elem dom] :
GetElem cont (Fin n) elem fun (xs : cont) (i : Fin n) => dom xs i
Equations
• instGetElemFinVal = { getElem := fun (xs : cont) (i : Fin n) (h : dom xs i) => xs[i] }