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

The type Fin 0 is uninhabited, so it can be used to derive any result whatsoever.

This is similar to Empty.elim. It can be thought of as a compiler-checked assertion that a code path is unreachable, or a logical contradiction from which False and thus anything else could be derived.

Equations

• ⟨val, h⟩.elim0 = absurd h ⋯

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

The successor, with an increased bound.

This differs from adding 1, which instead wraps around.

Examples:

• (2 : Fin 3).succ = (3 : Fin 4)
• (2 : Fin 3) + 1 = (0 : Fin 3)

Equations

• ⟨i, h⟩.succ = ⟨i + 1, ⋯⟩

def Fin.ofNat (n : Nat) [NeZero n] (a : Nat) : Fin n

Returns a modulo n as a Fin n.

The assumption NeZero n ensures that Fin n is nonempty.

Equations

• Fin.ofNat n a = ⟨a % n, ⋯⟩

@[simp]

theorem Fin.Internal.ofNat_eq_ofNat {n : Nat} {hn : 0 < n} {a : Nat} : Internal.ofNat n hn a = Fin.ofNat n a

@[deprecated Fin.ofNat (since := "2025-05-28")]

def Fin.ofNat' (n : Nat) [NeZero n] (a : Nat) : Fin n

Equations

• Fin.ofNat' n a = Fin.ofNat n a

@[inline]

def Fin.toNat {n : Nat} (i : Fin n) : Nat

Extracts the underlying Nat value.

This function is a synonym for Fin.val, which is the simp normal form. Fin.val is also a coercion, so values of type Fin n are automatically converted to Nats as needed.

Equations

• i.toNat = ↑i

@[simp]

theorem Fin.toNat_eq_val {n : Nat} {i : Fin n} : i.toNat = ↑i

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

Addition modulo n, usually invoked via the + operator.

Examples:

• (2 : Fin 8) + (2 : Fin 8) = (4 : Fin 8)
• (2 : Fin 3) + (2 : Fin 3) = (1 : Fin 3)

Equations

• ⟨a, h⟩.add ⟨b, isLt⟩ = ⟨(a + b) % n, ⋯⟩

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

Multiplication modulo n, usually invoked via the * operator.

Examples:

• (2 : Fin 10) * (2 : Fin 10) = (4 : Fin 10)
• (2 : Fin 10) * (7 : Fin 10) = (4 : Fin 10)
• (3 : Fin 10) * (7 : Fin 10) = (1 : Fin 10)

Equations

• ⟨a, h⟩.mul ⟨b, isLt⟩ = ⟨a * b % n, ⋯⟩

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

Subtraction modulo n, usually invoked via the - operator.

Examples:

• (5 : Fin 11) - (3 : Fin 11) = (2 : Fin 11)
• (3 : Fin 11) - (5 : Fin 11) = (9 : Fin 11)

Equations

• ⟨a, h⟩.sub ⟨b, isLt⟩ = ⟨(n - b + a) % n, ⋯⟩

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

Modulus of bounded numbers, usually invoked via the % operator.

The resulting value is that computed by the % operator on Nat.

Equations

• ⟨a, h⟩.mod ⟨b, isLt⟩ = ⟨a % b, ⋯⟩

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

Division of bounded numbers, usually invoked via the / operator.

The resulting value is that computed by the / operator on Nat. In particular, the result of division by 0 is 0.

Examples:

• (5 : Fin 10) / (2 : Fin 10) = (2 : Fin 10)
• (5 : Fin 10) / (0 : Fin 10) = (0 : Fin 10)
• (5 : Fin 10) / (7 : Fin 10) = (0 : Fin 10)

Equations

• ⟨a, h⟩.div ⟨b, isLt⟩ = ⟨a / b, ⋯⟩

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

Modulus of bounded numbers with respect to a Nat.

The resulting value is that computed by the % operator on Nat.

Equations

• ⟨a, h⟩.modn x✝ = ⟨a % x✝, ⋯⟩

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

Bitwise and.

Equations

• ⟨a, h⟩.land ⟨b, isLt⟩ = ⟨a.land b % n, ⋯⟩

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

Bitwise or.

Equations

• ⟨a, h⟩.lor ⟨b, isLt⟩ = ⟨a.lor b % n, ⋯⟩

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

Bitwise xor (“exclusive or”).

Equations

• ⟨a, h⟩.xor ⟨b, isLt⟩ = ⟨a.xor b % n, ⋯⟩

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

Bitwise left shift of bounded numbers, with wraparound on overflow.

Examples:

• (1 : Fin 10) <<< (1 : Fin 10) = (2 : Fin 10)
• (1 : Fin 10) <<< (3 : Fin 10) = (8 : Fin 10)
• (1 : Fin 10) <<< (4 : Fin 10) = (6 : Fin 10)

Equations

• ⟨a, h⟩.shiftLeft ⟨b, isLt⟩ = ⟨a <<< b % n, ⋯⟩

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

Bitwise right shift of bounded numbers.

This operator corresponds to logical rather than arithmetic bit shifting. The new bits are always 0.

Examples:

• (15 : Fin 16) >>> (1 : Fin 16) = (7 : Fin 16)
• (15 : Fin 16) >>> (2 : Fin 16) = (3 : Fin 16)
• (15 : Fin 17) >>> (2 : Fin 17) = (3 : Fin 17)

Equations

• ⟨a, h⟩.shiftRight ⟨b, isLt⟩ = ⟨a >>> b % n, ⋯⟩

instance Fin.instAdd {n : Nat} : Add (Fin n)

Equations

• Fin.instAdd = { add := Fin.add }

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

Equations

• Fin.instAndOp = { and := Fin.land }

instance Fin.instOrOp {n : Nat} : OrOp (Fin n)

Equations

• Fin.instOrOp = { or := Fin.lor }

instance Fin.instXorOp {n : Nat} : XorOp (Fin n)

Equations

• Fin.instXorOp = { xor := Fin.xor }

instance Fin.instShiftLeft {n : Nat} : ShiftLeft (Fin n)

Equations

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

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

Equations

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

instance Fin.instOfNat {n : Nat} [NeZero n] {i : Nat} : OfNat (Fin n) i

Equations

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

theorem Fin.pos {n : Nat} (i : Fin n) : 0 < n

If you actually have an element of Fin n, then the n is always positive

instance Fin.neg (n : Nat) : Neg (Fin n)

Negation on Fin n

Equations

• Fin.neg n = { neg := fun (a : Fin n) => ⟨(n - ↑a) % n, ⋯⟩ }

theorem Fin.neg_def {n : Nat} (a : Fin n) : -a = ⟨(n - ↑a) % n, ⋯⟩

theorem Fin.coe_neg {n : Nat} (a : Fin n) : ↑(-a) = (n - ↑a) % n

instance Fin.instInhabited {n : Nat} [NeZero n] : Inhabited (Fin n)

Equations

• Fin.instInhabited = { default := 0 }

@[simp]

theorem Fin.zero_eta {n : Nat} : ⟨0, ⋯⟩ = 0

theorem Fin.ne_of_val_ne {n : Nat} {i j : Fin n} (h : ↑i ≠ ↑j) : i ≠ j

theorem Fin.val_ne_of_ne {n : Nat} {i j : Fin n} (h : i ≠ j) : ↑i ≠ ↑j

theorem Fin.modn_lt {n m : Nat} (i : Fin n) : m > 0 → ↑(i.modn m) < m

theorem Fin.val_lt_of_le {n b : Nat} (i : Fin b) (h : b ≤ n) : ↑i < n

@[inline]

def Fin.last (n : Nat) : Fin (n + 1)

The greatest value of Fin (n+1), namely n.

Examples:

• Fin.last 4 = (4 : Fin 5)
• (Fin.last 0).val = (0 : Nat)

Equations

• Fin.last n = ⟨n, ⋯⟩

@[inline]

def Fin.castLT {n m : Nat} (i : Fin m) (h : ↑i < n) : Fin n

Replaces the bound with another that is suitable for the value.

The proof embedded in i can be used to cast to a larger bound even if the concrete value is not known.

Examples:

example : Fin 12 := (7 : Fin 10).castLT (by decide : 7 < 12)

example (i : Fin 10) : Fin 12 :=
  i.castLT <| by
    cases i; simp; omega

Equations

• i.castLT h = ⟨↑i, h⟩

@[inline]

def Fin.castLE {n m : Nat} (h : n ≤ m) (i : Fin n) : Fin m

Coarsens a bound to one at least as large.

See also Fin.castAdd for a version that represents the larger bound with addition rather than an explicit inequality proof.

Equations

• Fin.castLE h i = ⟨↑i, ⋯⟩

@[inline]

def Fin.cast {n m : Nat} (eq : n = m) (i : Fin n) : Fin m

Uses a proof that two bounds are equal to allow a value bounded by one to be used with the other.

In other words, when eq : n = m, Fin.cast eq i converts i : Fin n into a Fin m.

Equations

• Fin.cast eq i = ⟨↑i, ⋯⟩

@[inline]

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

Coarsens a bound to one at least as large.

See also Fin.natAdd and Fin.addNat for addition functions that increase the bound, and Fin.castLE for a version that uses an explicit inequality proof.

Equations

• Fin.castAdd m = Fin.castLE ⋯

@[inline]

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

Coarsens a bound by one.

Equations

• Fin.castSucc = Fin.castAdd 1

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

Adds a natural number to a Fin, increasing the bound.

This is a generalization of Fin.succ.

Fin.natAdd is a version of this function that takes its Nat parameter first.

Examples:

• Fin.addNat (5 : Fin 8) 3 = (8 : Fin 11)
• Fin.addNat (0 : Fin 8) 1 = (1 : Fin 9)
• Fin.addNat (1 : Fin 8) 2 = (3 : Fin 10)

Equations

• i.addNat m = ⟨↑i + m, ⋯⟩

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

Adds a natural number to a Fin, increasing the bound.

This is a generalization of Fin.succ.

Fin.addNat is a version of this function that takes its Nat parameter second.

Examples:

• Fin.natAdd 3 (5 : Fin 8) = (8 : Fin 11)
• Fin.natAdd 1 (0 : Fin 8) = (1 : Fin 9)
• Fin.natAdd 1 (2 : Fin 8) = (3 : Fin 9)

Equations

• Fin.natAdd n i = ⟨n + ↑i, ⋯⟩

@[inline]

def Fin.rev {n : Nat} (i : Fin n) : Fin n

Replaces a value with its difference from the largest value in the type.

Considering the values of Fin n as a sequence 0, 1, …, n-2, n-1, Fin.rev finds the corresponding element of the reversed sequence. In other words, it maps 0 to n-1, 1 to n-2, ..., and n-1 to 0.

Examples:

• (5 : Fin 6).rev = (0 : Fin 6)
• (0 : Fin 6).rev = (5 : Fin 6)
• (2 : Fin 5).rev = (2 : Fin 5)

Equations

• i.rev = ⟨n - (↑i + 1), ⋯⟩

@[inline]

def Fin.subNat {n : Nat} (m : Nat) (i : Fin (n + m)) (h : m ≤ ↑i) : Fin n

Subtraction of a natural number from a Fin, with the bound narrowed.

This is a generalization of Fin.pred. It is guaranteed to not underflow or wrap around.

Examples:

• (5 : Fin 9).subNat 2 (by decide) = (3 : Fin 7)
• (5 : Fin 9).subNat 0 (by decide) = (5 : Fin 9)
• (3 : Fin 9).subNat 3 (by decide) = (0 : Fin 6)

Equations

• Fin.subNat m i h = ⟨↑i - m, ⋯⟩

@[inline]

def Fin.pred {n : Nat} (i : Fin (n + 1)) (h : i ≠ 0) : Fin n

The predecessor of a non-zero element of Fin (n+1), with the bound decreased.

Examples:

• (4 : Fin 8).pred (by decide) = (3 : Fin 7)
• (1 : Fin 2).pred (by decide) = (0 : Fin 1)

Equations

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

theorem Fin.val_inj {n : Nat} {a b : Fin n} : ↑a = ↑b ↔ a = b

theorem Fin.val_congr {n : Nat} {a b : Fin n} (h : a = b) : ↑a = ↑b

theorem Fin.val_le_of_le {n : Nat} {a b : Fin n} (h : a ≤ b) : ↑a ≤ ↑b

theorem Fin.val_le_of_ge {n : Nat} {a b : Fin n} (h : a ≥ b) : ↑b ≤ ↑a

theorem Fin.val_add_one_le_of_lt {n : Nat} {a b : Fin n} (h : a < b) : ↑a + 1 ≤ ↑b

theorem Fin.val_add_one_le_of_gt {n : Nat} {a b : Fin n} (h : a > b) : ↑b + 1 ≤ ↑a

theorem Fin.exists_iff {n : Nat} {p : Fin n → Prop} : (∃ (i : Fin n), p i) ↔ ∃ (i : Nat), ∃ (h : i < n), p ⟨i, h⟩