instance Fin.coeToNat {n : Nat} : CoeOut (Fin n) Nat

Equations

• Fin.coeToNat = { coe := fun (v : Fin n) => ↑v }

def Fin.elim0 {α : Sort u} : Fin 0 → α

Equations

• Fin.elim0 x = match x with | { val := val, isLt := h } => absurd h ⋯

def Fin.succ {n : Nat} : Fin n → Fin (Nat.succ n)

Equations

• Fin.succ x = match x with | { val := i, isLt := h } => { val := i + 1, isLt := ⋯ }

def Fin.ofNat {n : Nat} (a : Nat) : Fin (Nat.succ n)

Equations

• Fin.ofNat a = { val := a % (n + 1), isLt := ⋯ }

def Fin.ofNat' {n : Nat} (a : Nat) (h : n > 0) : Fin n

Equations

• Fin.ofNat' a h = { val := a % n, isLt := ⋯ }

def Fin.add {n : Nat} : Fin n → Fin n → Fin n

Equations

• Fin.add x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := (a + b) % n, isLt := ⋯ }

def Fin.mul {n : Nat} : Fin n → Fin n → Fin n

Equations

• Fin.mul x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a * b % n, isLt := ⋯ }

def Fin.sub {n : Nat} : Fin n → Fin n → Fin n

Equations

• Fin.sub x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := (a + (n - b)) % n, isLt := ⋯ }

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 n → Fin n → Fin n

Equations

• Fin.mod x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a % b, isLt := ⋯ }

def Fin.div {n : Nat} : Fin n → Fin n → Fin n

Equations

• Fin.div x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a / b, isLt := ⋯ }

def Fin.modn {n : Nat} : Fin n → Nat → Fin n

Equations

• Fin.modn x✝ x = match x✝, x with | { val := a, isLt := h }, m => { val := a % m, isLt := ⋯ }

def Fin.land {n : Nat} : Fin n → Fin n → Fin 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 := ⋯ }

def Fin.lor {n : Nat} : Fin n → Fin n → Fin 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 := ⋯ }

def Fin.xor {n : Nat} : Fin n → Fin n → Fin 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 := ⋯ }

def Fin.shiftLeft {n : Nat} : Fin n → Fin n → Fin n

Equations

• Fin.shiftLeft x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a <<< b % n, isLt := ⋯ }

def Fin.shiftRight {n : Nat} : Fin n → Fin n → Fin n

Equations

• Fin.shiftRight x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a >>> b % n, isLt := ⋯ }

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} : AndOp (Fin n)

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} : ShiftLeft (Fin n)

Equations

• Fin.instShiftLeftFin = { shiftLeft := Fin.shiftLeft }

instance Fin.instShiftRightFin {n : Nat} : ShiftRight (Fin n)

Equations

• Fin.instShiftRightFin = { shiftRight := Fin.shiftRight }

instance Fin.instOfNat {n : Nat} {i : Nat} : OfNat (Fin (n + 1)) i

Equations

• Fin.instOfNat = { ofNat := Fin.ofNat i }

instance Fin.instInhabitedFinHAddNatInstHAddInstAddNatOfNat {n : Nat} : Inhabited (Fin (n + 1))

Equations

• Fin.instInhabitedFinHAddNatInstHAddInstAddNatOfNat = { default := 0 }

@[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

• Fin.last n = { val := n, isLt := ⋯ }

@[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

• Fin.castLT i h = { val := ↑i, isLt := h }

@[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

• Fin.castLE h i = { val := ↑i, isLt := ⋯ }

@[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

• Fin.cast eq i = { val := ↑i, isLt := ⋯ }

@[inline]

def Fin.castAdd {n : Nat} (m : Nat) : Fin n → Fin (n + m)

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

Equations

• Fin.castAdd m = Fin.castLE ⋯

@[inline]

def Fin.castSucc {n : Nat} : Fin n → Fin (n + 1)

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

Equations

• Fin.castSucc = Fin.castAdd 1

def Fin.addNat {n : Nat} (i : Fin n) (m : Nat) : Fin (n + m)

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

Equations

• Fin.addNat i m = { val := ↑i + m, isLt := ⋯ }

def Fin.natAdd {m : Nat} (n : Nat) (i : Fin m) : Fin (n + m)

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

Equations

• Fin.natAdd n i = { val := n + ↑i, isLt := ⋯ }

@[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

• Fin.rev i = { val := n - (↑i + 1), isLt := ⋯ }

@[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

• Fin.subNat m i h = { val := ↑i - m, isLt := ⋯ }

@[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

• Fin.pred i h = Fin.subNat 1 i ⋯

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 → Nat → Prop} {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] }