The finite type with n elements

Fin n is the type whose elements are natural numbers smaller than n. This file expands on the development in the core library.

Main definitions

• finZeroElim : Elimination principle for the empty set Fin 0, generalizes Fin.elim0. Further definitions and eliminators can be found in Init.Data.Fin.Lemmas
• Fin.equivSubtype : Equivalence between Fin n and { i // i < n }.
• Fin.divNat i : divides i : Fin (m * n) by n;
• Fin.modNat i : takes the mod of i : Fin (m * n) by n;

def finZeroElim {α : Fin 0 → Sort u_1} (x : Fin 0) : α x

Elimination principle for the empty set Fin 0, dependent version.

Equations

• finZeroElim x = x.elim0

@[simp]

theorem Fin.mk_eq_one {n a : ℕ} {ha : a < n + 2} : ⟨a, ha⟩ = 1 ↔ a = 1

@[simp]

theorem Fin.one_eq_mk {n a : ℕ} {ha : a < n + 2} : 1 = ⟨a, ha⟩ ↔ a = 1

instance Fin.instCanLiftNatValLt {n : ℕ} : CanLift ℕ (Fin n) val fun (x : ℕ) => x < n

def Fin.rec0 {α : Fin 0 → Sort u_1} (i : Fin 0) : α i

A dependent variant of Fin.elim0.

Equations

• i.rec0 = absurd ⋯ ⋯

theorem Fin.val_injective {n : ℕ} : Function.Injective val

theorem Fin.size_positive {n : ℕ} : ∀ (a : Fin n), 0 < n

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

theorem Fin.size_positive' {n : ℕ} [Nonempty (Fin n)] : 0 < n

theorem Fin.prop {n : ℕ} (a : Fin n) : ↑a < n

theorem Fin.lt_last_iff_ne_last {n : ℕ} {a : Fin (n + 1)} : a < last n ↔ a ≠ last n

theorem Fin.ne_zero_of_lt {n : ℕ} {a b : Fin (n + 1)} (hab : a < b) : b ≠ 0

theorem Fin.ne_last_of_lt {n : ℕ} {a b : Fin (n + 1)} (hab : a < b) : a ≠ last n

def Fin.equivSubtype {n : ℕ} : Fin n ≃ { i : ℕ // i < n }

Equivalence between Fin n and { i // i < n }.

Equations

• Fin.equivSubtype = { toFun := fun (a : Fin n) => ⟨↑a, ⋯⟩, invFun := fun (a : { i : ℕ // i < n }) => ⟨↑a, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Fin.equivSubtype_apply {n : ℕ} (a : Fin n) : equivSubtype a = ⟨↑a, ⋯⟩

@[simp]

theorem Fin.equivSubtype_symm_apply {n : ℕ} (a : { i : ℕ // i < n }) : equivSubtype.symm a = ⟨↑a, ⋯⟩

coercions and constructions

theorem Fin.val_eq_val {n : ℕ} (a b : Fin n) : ↑a = ↑b ↔ a = b

theorem Fin.ne_iff_vne {n : ℕ} (a b : Fin n) : a ≠ b ↔ ↑a ≠ ↑b

theorem Fin.mk_eq_mk {n a : ℕ} {h : a < n} {a' : ℕ} {h' : a' < n} : ⟨a, h⟩ = ⟨a', h'⟩ ↔ a = a'

theorem Fin.heq_fun_iff {α : Sort u_1} {k l : ℕ} (h : k = l) {f : Fin k → α} {g : Fin l → α} : f ≍ g ↔ ∀ (i : Fin k), f i = g ⟨↑i, ⋯⟩

Assume k = l. If two functions defined on Fin k and Fin l are equal on each element, then they coincide (in the heq sense).

theorem Fin.heq_fun₂_iff {α : Sort u_1} {k l k' l' : ℕ} (h : k = l) (h' : k' = l') {f : Fin k → Fin k' → α} {g : Fin l → Fin l' → α} : f ≍ g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩

Assume k = l and k' = l'. If two functions Fin k → Fin k' → α and Fin l → Fin l' → α are equal on each pair, then they coincide (in the heq sense).

theorem Fin.heq_ext_iff {k l : ℕ} (h : k = l) {i : Fin k} {j : Fin l} : i ≍ j ↔ ↑i = ↑j

Two elements of Fin k and Fin l are heq iff their values in ℕ coincide. This requires k = l. For the left implication without this assumption, see val_eq_val_of_heq.

order

theorem Fin.lt_or_ge {n : ℕ} (a b : Fin n) : a < b ∨ b ≤ a

Fin.lt_or_ge is an alias of Fin.lt_or_le. It is preferred since it follows the mathlib naming convention.

theorem Fin.le_or_gt {n : ℕ} (a b : Fin n) : a ≤ b ∨ b < a

Fin.le_or_gt is an alias of Fin.le_or_lt. It is preferred since it follows the mathlib naming convention.

theorem Fin.le_iff_val_le_val {n : ℕ} {a b : Fin n} : a ≤ b ↔ ↑a ≤ ↑b

@[simp]

theorem Fin.val_fin_lt {n : ℕ} {a b : Fin n} : ↑a < ↑b ↔ a < b

a < b as natural numbers if and only if a < b in Fin n.

@[simp]

theorem Fin.val_fin_le {n : ℕ} {a b : Fin n} : ↑a ≤ ↑b ↔ a ≤ b

a ≤ b as natural numbers if and only if a ≤ b in Fin n.

theorem Fin.min_val {n : ℕ} {a : Fin n} : min (↑a) n = ↑a

theorem Fin.max_val {n : ℕ} {a : Fin n} : max (↑a) n = n

instance Fin.instWellFoundedRelation_mathlib {n : ℕ} : WellFoundedRelation (Fin n)

Use the ordering on Fin n for checking recursive definitions.

For example, the following definition is not accepted by the termination checker, unless we declare the WellFoundedRelation instance:

def factorial {n : ℕ} : Fin n → ℕ
  | ⟨0, _⟩ := 1
  | ⟨i + 1, hi⟩ := (i + 1) * factorial ⟨i, i.lt_succ_self.trans hi⟩

Equations

• Fin.instWellFoundedRelation_mathlib = measure Fin.val

@[deprecated Fin.val_zero (since := "2025-02-24")]

theorem Fin.val_zero' (n : ℕ) [NeZero n] : ↑0 = 0

Alias of Fin.val_zero.

@[simp]

theorem Fin.mk_zero' (n : ℕ) [NeZero n] : ⟨0, ⋯⟩ = 0

Fin.mk_zero in Lean only applies in Fin (n + 1). This one instead uses a NeZero n typeclass hypothesis.

@[deprecated Fin.zero_le (since := "2025-05-13")]

theorem Fin.zero_le' {n : ℕ} [NeZero n] (a : Fin n) : 0 ≤ a

@[simp]

theorem Fin.val_pos_iff {n : ℕ} [NeZero n] {a : Fin n} : 0 < ↑a ↔ 0 < a

theorem Fin.pos_iff_ne_zero' {n : ℕ} [NeZero n] (a : Fin n) : 0 < a ↔ a ≠ 0

The Fin.pos_iff_ne_zero in Lean only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

@[simp]

theorem Fin.cast_eq_self {n : ℕ} (a : Fin n) : Fin.cast ⋯ a = a

@[simp]

theorem Fin.cast_eq_zero {k l : ℕ} [NeZero k] [NeZero l] (h : k = l) (x : Fin k) : Fin.cast h x = 0 ↔ x = 0

theorem Fin.cast_injective {k l : ℕ} (h : k = l) : Function.Injective (Fin.cast h)

theorem Fin.last_pos' {n : ℕ} [NeZero n] : 0 < last n

theorem Fin.one_lt_last {n : ℕ} [NeZero n] : 1 < last (n + 1)

Coercions to ℤ and the fin_omega tactic.

theorem Fin.coe_int_sub_eq_ite {n : ℕ} (u v : Fin n) : ↑↑(u - v) = if v ≤ u then ↑↑u - ↑↑v else ↑↑u - ↑↑v + ↑n

theorem Fin.coe_int_sub_eq_mod {n : ℕ} (u v : Fin n) : ↑↑(u - v) = (↑↑u - ↑↑v) % ↑n

theorem Fin.coe_int_add_eq_ite {n : ℕ} (u v : Fin n) : ↑↑(u + v) = if ↑u + ↑v < n then ↑↑u + ↑↑v else ↑↑u + ↑↑v - ↑n

theorem Fin.coe_int_add_eq_mod {n : ℕ} (u v : Fin n) : ↑↑(u + v) = (↑↑u + ↑↑v) % ↑n

def Fin.tacticFin_omega : Lean.ParserDescr

Preprocessor for omega to handle inequalities in Fin. Note that this involves a lot of case splitting, so may be slow.

Equations

• Fin.tacticFin_omega = Lean.ParserDescr.node `Fin.tacticFin_omega 1024 (Lean.ParserDescr.nonReservedSymbol "fin_omega" false)

addition, numerals, and coercion from Nat

theorem Fin.val_one' (n : ℕ) [NeZero n] : ↑1 = 1 % n

@[deprecated Fin.val_one' (since := "2025-03-10")]

theorem Fin.val_one'' {n : ℕ} : ↑1 = 1 % (n + 1)

theorem Fin.nontrivial_iff_two_le {n : ℕ} : Nontrivial (Fin n) ↔ 2 ≤ n

instance Fin.instNontrivial {n : ℕ} [n.AtLeastTwo] : Nontrivial (Fin n)

theorem Fin.exists_ne_and_ne_of_two_lt {n : ℕ} (i j : Fin n) (h : 2 < n) : ∃ (k : Fin n), k ≠ i ∧ k ≠ j

If working with more than two elements, we can always pick a third distinct from two existing elements.

instance Fin.inhabitedFinOneAdd (n : ℕ) : Inhabited (Fin (1 + n))

Equations

• Fin.inhabitedFinOneAdd n = inferInstance

@[simp]

theorem Fin.default_eq_zero (n : ℕ) [NeZero n] : default = 0

theorem Fin.val_add_eq_ite {n : ℕ} (a b : Fin n) : ↑(a + b) = if n ≤ ↑a + ↑b then ↑a + ↑b - n else ↑a + ↑b

theorem Fin.val_add_eq_of_add_lt {n : ℕ} {a b : Fin n} (huv : ↑a + ↑b < n) : ↑(a + b) = ↑a + ↑b

theorem Fin.intCast_val_sub_eq_sub_add_ite {n : ℕ} (a b : Fin n) : ↑↑(a - b) = ↑↑a - ↑↑b + ↑(if b ≤ a then 0 else n)

theorem Fin.sub_val_lt_sub {n : ℕ} {i j : Fin n} (hij : i ≤ j) : ↑(j - i) < n - ↑i

theorem Fin.castLT_sub_nezero {n : ℕ} {i j : Fin n} (hij : i < j) : (j - i).castLT ⋯ ≠ 0

theorem Fin.one_le_of_ne_zero {n : ℕ} [NeZero n] {k : Fin n} (hk : k ≠ 0) : 1 ≤ k

theorem Fin.val_sub_one_of_ne_zero {n : ℕ} [NeZero n] {i : Fin n} (hi : i ≠ 0) : ↑(i - 1) = ↑i - 1

@[simp]

theorem Fin.ofNat_eq_cast (n : ℕ) [NeZero n] (a : ℕ) : Fin.ofNat n a = ↑a

@[deprecated Fin.ofNat_eq_cast (since := "2025-05-30")]

theorem Fin.ofNat'_eq_cast (n : ℕ) [NeZero n] (a : ℕ) : Fin.ofNat n a = ↑a

Alias of Fin.ofNat_eq_cast.

@[simp]

theorem Fin.val_natCast (a n : ℕ) [NeZero n] : ↑↑a = a % n

theorem Fin.val_cast_of_lt {n : ℕ} [NeZero n] {a : ℕ} (h : a < n) : ↑↑a = a

Converting an in-range number to Fin (n + 1) produces a result whose value is the original number.

@[simp]

theorem Fin.cast_val_eq_self {n : ℕ} [NeZero n] (a : Fin n) : ↑↑a = a

If n is non-zero, converting the value of a Fin n to Fin n results in the same value.

@[simp]

theorem Fin.natCast_self (n : ℕ) [NeZero n] : ↑n = 0

@[simp]

theorem Fin.natCast_eq_zero {a n : ℕ} [NeZero n] : ↑a = 0 ↔ n ∣ a

@[simp]

theorem Fin.natCast_eq_last (n : ℕ) : ↑n = last n

theorem Fin.natCast_eq_mk {m n : ℕ} (h : m < n) : have this := ⋯; ↑m = ⟨m, h⟩

theorem Fin.one_eq_mk_of_lt {n : ℕ} (h : 1 < n) : have this := ⋯; 1 = ⟨1, h⟩

theorem Fin.le_val_last {n : ℕ} (i : Fin (n + 1)) : i ≤ ↑n

theorem Fin.natCast_le_natCast {n a b : ℕ} (han : a ≤ n) (hbn : b ≤ n) : ↑a ≤ ↑b ↔ a ≤ b

theorem Fin.natCast_lt_natCast {n a b : ℕ} (han : a ≤ n) (hbn : b ≤ n) : ↑a < ↑b ↔ a < b

theorem Fin.natCast_mono {n a b : ℕ} (hbn : b ≤ n) (hab : a ≤ b) : ↑a ≤ ↑b

theorem Fin.natCast_strictMono {n a b : ℕ} (hbn : b ≤ n) (hab : a < b) : ↑a < ↑b

@[simp]

theorem Fin.castLE_natCast {m n : ℕ} [NeZero m] (h : m ≤ n) (a : ℕ) : castLE h ↑a = ↑(a % m)

def Fin.divNat {n m : ℕ} (i : Fin (m * n)) : Fin m

Compute i / n, where n is a Nat and inferred the type of i.

Equations

• i.divNat = ⟨↑i / n, ⋯⟩

@[simp]

theorem Fin.coe_divNat {n m : ℕ} (i : Fin (m * n)) : ↑i.divNat = ↑i / n

def Fin.modNat {n m : ℕ} (i : Fin (m * n)) : Fin n

Compute i % n, where n is a Nat and inferred the type of i.

Equations

• i.modNat = ⟨↑i % n, ⋯⟩

@[simp]

theorem Fin.coe_modNat {n m : ℕ} (i : Fin (m * n)) : ↑i.modNat = ↑i % n

theorem Fin.modNat_rev {n m : ℕ} (i : Fin (m * n)) : i.rev.modNat = i.modNat.rev

recursion and induction principles

theorem Fin.liftFun_iff_succ {n : ℕ} {α : Type u_1} (r : α → α → Prop) [IsTrans α r] {f : Fin (n + 1) → α} : Relator.LiftFun (fun (x1 x2 : Fin (n + 1)) => x1 < x2) r f f ↔ ∀ (i : Fin n), r (f i.castSucc) (f i.succ)

theorem Fin.eq_zero (n : Fin 1) : n = 0

theorem Fin.eq_one_of_ne_zero (i : Fin 2) (hi : i ≠ 0) : i = 1

@[deprecated Fin.eq_one_of_ne_zero (since := "2025-04-27")]

theorem Fin.eq_one_of_neq_zero (i : Fin 2) (hi : i ≠ 0) : i = 1

Alias of Fin.eq_one_of_ne_zero.

@[simp]

theorem Fin.coe_neg_one {n : ℕ} : ↑(-1) = n

theorem Fin.last_sub {n : ℕ} (i : Fin (n + 1)) : last n - i = i.rev

theorem Fin.add_one_le_of_lt {n : ℕ} {a b : Fin (n + 1)} (h : a < b) : a + 1 ≤ b

theorem Fin.exists_eq_add_of_le {n : ℕ} {a b : Fin n} (h : a ≤ b) : ∃ (k : Fin n), k ≤ b ∧ b = a + k

theorem Fin.exists_eq_add_of_lt {n : ℕ} {a b : Fin (n + 1)} (h : a < b) : ∃ (k : Fin (n + 1)), k < b ∧ k + 1 ≤ b ∧ b = a + k + 1

theorem Fin.pos_of_ne_zero {n : ℕ} {a : Fin (n + 1)} (h : a ≠ 0) : 0 < a

theorem Fin.sub_succ_le_sub_of_le {n : ℕ} {u v : Fin (n + 2)} (h : u < v) : v - (u + 1) < v - u

@[simp]

theorem Fin.coe_natCast_eq_mod (m n : ℕ) [NeZero m] : ↑↑n = n % m

@[simp]

theorem Fin.coe_ofNat_eq_mod (m n : ℕ) [NeZero m] : ↑(OfNat.ofNat n) = OfNat.ofNat n % m

theorem Fin.val_add_one_of_lt' {n : ℕ} [NeZero n] {i : Fin n} (h : ↑i + 1 < n) : ↑(i + 1) = ↑i + 1

instance Fin.instNeZeroHAddNatOfNat_mathlib {n m : ℕ} [NeZero n] [NeZero (OfNat.ofNat m)] : NeZero (OfNat.ofNat m)

mul

theorem Fin.mul_one' {n : ℕ} [NeZero n] (k : Fin n) : k * 1 = k

theorem Fin.one_mul' {n : ℕ} [NeZero n] (k : Fin n) : 1 * k = k

theorem Fin.mul_zero' {n : ℕ} [NeZero n] (k : Fin n) : k * 0 = 0

theorem Fin.zero_mul' {n : ℕ} [NeZero n] (k : Fin n) : 0 * k = 0