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

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

source
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 ⋯

Instances For

source
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, ⋯⟩

Instances For

source
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, ⋯⟩

Instances For

source
@[simp]
theorem Fin.Internal.ofNat_eq_ofNat {n : Nat} {hn : 0 < n} {a : Nat} :
Internal.ofNat n hn a = Fin.ofNat n a
source
@[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

Instances For

source
@[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 `Nat`s as needed.

Equations

- i.toNat = ↑i

Instances For

source
@[simp]
theorem Fin.toNat_eq_val {n : Nat} {i : Fin n} :
i.toNat = ↑i
source
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, ⋯⟩

Instances For

source
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, ⋯⟩

Instances For

source
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, ⋯⟩

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.

source
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, ⋯⟩

Instances For

source
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, ⋯⟩

Instances For

source
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✝, ⋯⟩

Instances For

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

Bitwise and.

Equations

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

Instances For

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

Bitwise or.

Equations

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

Instances For

source
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, ⋯⟩

Instances For

source
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, ⋯⟩

Instances For

source
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, ⋯⟩

Instances For

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

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

source
instance Fin.instSub {n : Nat} :
Sub (Fin n)
Equations

- Fin.instSub = { sub := Fin.sub }

source
instance Fin.instMul {n : Nat} :
Mul (Fin n)
Equations

- Fin.instMul = { mul := Fin.mul }

source
instance Fin.instMod {n : Nat} :
Mod (Fin n)
Equations

- Fin.instMod = { mod := Fin.mod }

source
instance Fin.instDiv {n : Nat} :
Div (Fin n)
Equations

- Fin.instDiv = { div := Fin.div }

source
instance Fin.instAndOp {n : Nat} :
AndOp (Fin n)
Equations

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

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

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

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

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

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

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

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

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

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

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

source
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

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

Negation on `Fin n`

Equations

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

source
theorem Fin.neg_def {n : Nat} (a : Fin n) :
-a = ⟨(n - ↑a) % n, ⋯⟩
source
theorem Fin.coe_neg {n : Nat} (a : Fin n) :
↑(-a) = (n - ↑a) % n
source
instance Fin.instInhabited {n : Nat} [NeZero n] :
Inhabited (Fin n)
Equations

- Fin.instInhabited = { default := 0 }

source
@[simp]
theorem Fin.zero_eta {n : Nat} :
⟨0, ⋯⟩ = 0
source
theorem Fin.ne_of_val_ne {n : Nat} {i j : Fin n} (h : ↑i ≠ ↑j) :
i ≠ j
source
theorem Fin.val_ne_of_ne {n : Nat} {i j : Fin n} (h : i ≠ j) :
↑i ≠ ↑j
source
theorem Fin.modn_lt {n m : Nat} (i : Fin n) :
m > 0 → ↑(i.modn m) < m
source
theorem Fin.val_lt_of_le {n b : Nat} (i : Fin b) (h : b ≤ n) :
↑i < n
source
@[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, ⋯⟩

Instances For

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

Instances For

source
@[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, ⋯⟩

Instances For

source
@[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, ⋯⟩

Instances For

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

Instances For

source
@[inline]
def Fin.castSucc {n : Nat} :
Fin n → Fin (n + 1)

Coarsens a bound by one.

Equations

- Fin.castSucc = Fin.castAdd 1

Instances For

source
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, ⋯⟩

Instances For

source
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, ⋯⟩

Instances For

source
@[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), ⋯⟩

Instances For

source
@[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, ⋯⟩

Instances For

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

Instances For

source
theorem Fin.val_inj {n : Nat} {a b : Fin n} :
↑a = ↑b ↔ a = b
source
theorem Fin.val_congr {n : Nat} {a b : Fin n} (h : a = b) :
↑a = ↑b
source
theorem Fin.val_le_of_le {n : Nat} {a b : Fin n} (h : a ≤ b) :
↑a ≤ ↑b
source
theorem Fin.val_le_of_ge {n : Nat} {a b : Fin n} (h : a ≥ b) :
↑b ≤ ↑a
source
theorem Fin.val_add_one_le_of_lt {n : Nat} {a b : Fin n} (h : a < b) :
↑a + 1 ≤ ↑b
source
theorem Fin.val_add_one_le_of_gt {n : Nat} {a b : Fin n} (h : a > b) :
↑b + 1 ≤ ↑a
source
theorem Fin.exists_iff {n : Nat} {p : Fin n → Prop} :
(∃ (i : Fin n), p i) ↔ ∃ (i : Nat), ∃ (h : i < n), p ⟨i, h⟩