# 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α

From the empty type Fin 0, any desired result α can be derived. This is simlar to Empty.elim.

Equations
Instances For
def Fin.succ {n : Nat} :
Fin nFin n.succ

Returns the successor of the argument.

The bound in the result type is increased:

(2 : Fin 3).succ = (3 : Fin 4)


This differs from addition, which wraps around:

(2 : Fin 3) + 1 = (0 : Fin 3)

Equations
• i, h.succ = i + 1,
Instances For
def Fin.ofNat {n : Nat} (a : Nat) :
Fin n.succ

Returns a modulo n + 1 as a Fin n.succ.

Equations
• = a % (n + 1),
Instances For
def Fin.ofNat' {n : Nat} (a : Nat) (h : n > 0) :
Fin n

Returns a modulo n as a Fin n.

The assumption n > 0 ensures that Fin n is nonempty.

Equations
• = a % n,
Instances For
def Fin.add {n : Nat} :
Fin nFin nFin n

Addition modulo n

Equations
• a, h.add b, isLt = (a + b) % n,
Instances For
def Fin.mul {n : Nat} :
Fin nFin nFin n

Multiplication modulo n

Equations
• a, h.mul b, isLt = a * b % n,
Instances For
def Fin.sub {n : Nat} :
Fin nFin nFin n

Subtraction modulo n

Equations
• a, h.sub b, isLt = (n - b + a) % n,
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
• a, h.mod b, isLt = a % b,
Instances For
def Fin.div {n : Nat} :
Fin nFin nFin n
Equations
• a, h.div b, isLt = a / b,
Instances For
def Fin.modn {n : Nat} :
Fin nNatFin n
Equations
• a, h.modn x = a % x,
Instances For
def Fin.land {n : Nat} :
Fin nFin nFin n
Equations
• a, h.land b, isLt = a.land b % n,
Instances For
def Fin.lor {n : Nat} :
Fin nFin nFin n
Equations
• a, h.lor b, isLt = a.lor b % n,
Instances For
def Fin.xor {n : Nat} :
Fin nFin nFin n
Equations
• a, h.xor b, isLt = a.xor b % n,
Instances For
def Fin.shiftLeft {n : Nat} :
Fin nFin nFin n
Equations
• a, h.shiftLeft b, isLt = a <<< b % n,
Instances For
def Fin.shiftRight {n : Nat} :
Fin nFin nFin n
Equations
• a, h.shiftRight b, isLt = a >>> b % n,
Instances For
instance Fin.instAdd {n : Nat} :
Equations
instance Fin.instSub {n : Nat} :
Sub (Fin n)
Equations
• Fin.instSub = { sub := Fin.sub }
instance Fin.instMul {n : Nat} :
Mul (Fin n)
Equations
• Fin.instMul = { mul := Fin.mul }
instance Fin.instMod {n : Nat} :
Mod (Fin n)
Equations
• Fin.instMod = { mod := Fin.mod }
instance Fin.instDiv {n : Nat} :
Div (Fin n)
Equations
• Fin.instDiv = { div := Fin.div }
instance Fin.instAndOp {n : Nat} :
Equations
• Fin.instAndOp = { and := Fin.land }
instance Fin.instOrOp {n : Nat} :
OrOp (Fin n)
Equations
• Fin.instOrOp = { or := Fin.lor }
instance Fin.instXor {n : Nat} :
Xor (Fin n)
Equations
• Fin.instXor = { xor := Fin.xor }
instance Fin.instShiftLeft {n : Nat} :
Equations
• Fin.instShiftLeft = { shiftLeft := Fin.shiftLeft }
instance Fin.instShiftRight {n : Nat} :
Equations
• Fin.instShiftRight = { shiftRight := Fin.shiftRight }
instance Fin.instOfNat {n : Nat} {i : Nat} :
OfNat (Fin (n + 1)) i
Equations
• Fin.instOfNat = { ofNat := }
Equations
• Fin.instInhabitedHAddNatOfNat = { default := 0 }
@[simp]
theorem Fin.zero_eta {n : Nat} :
0, = 0
theorem Fin.ne_of_val_ne {n : Nat} {i : Fin n} {j : Fin n} (h : i j) :
i j
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(i.modn 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
• = n,
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
• i.castLT h = i, 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
• = i,
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)

castAdd m i embeds i : Fin n in Fin (n+m). See also Fin.natAdd and Fin.addNat.

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
• i.addNat m = i + m,
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
• = n + i,
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
• i.rev = n - (i + 1),
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
theorem Fin.exists_iff {n : Nat} {p : Fin nProp} :
(∃ (i : Fin n), p i) ∃ (i : Nat), ∃ (h : i < n), p i, h