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

### Induction principles #

• finZeroElim : Elimination principle for the empty set Fin 0, generalizes Fin.elim0.
• Fin.succRec : Define C n i by induction on i : Fin n interpreted as (0 : Fin (n - i)).succ.succ…. This function has two arguments: H0 n defines 0-th element C (n+1) 0 of an (n+1)-tuple, and Hs n i defines (i+1)-st element of (n+1)-tuple based on n, i, and i-th element of n-tuple.
• Fin.succRecOn : same as Fin.succRec but i : Fin n is the first argument;
• Fin.induction : Define C i by induction on i : Fin (n + 1), separating into the Nat-like base cases of C 0 and C (i.succ).
• Fin.inductionOn : same as Fin.induction but with i : Fin (n + 1) as the first argument.
• Fin.cases : define f : Π i : Fin n.succ, C i by separately handling the cases i = 0 and i = Fin.succ j, j : Fin n, defined using Fin.induction.
• Fin.reverseInduction: reverse induction on i : Fin (n + 1); given C (Fin.last n) and ∀ i : Fin n, C (Fin.succ i) → C (Fin.castSucc i), constructs all values C i by going down;
• Fin.lastCases: define f : Π i, Fin (n + 1), C i by separately handling the cases i = Fin.last n and i = Fin.castSucc j, a special case of Fin.reverseInduction;
• Fin.addCases: define a function on Fin (m + n) by separately handling the cases Fin.castAdd n i and Fin.natAdd m i;
• Fin.succAboveCases: given i : Fin (n + 1), define a function on Fin (n + 1) by separately handling the cases j = i and j = Fin.succAbove i k, same as Fin.insertNth but marked as eliminator and works for Sort*. -- Porting note: this is in another file

### Embeddings and isomorphisms #

• Fin.valEmbedding : coercion to natural numbers as an Embedding;
• Fin.succEmb : Fin.succ as an Embedding;
• Fin.castLEEmb h : Fin.castLE as an Embedding, embed Fin n into Fin m, h : n ≤ m;
• finCongr : Fin.cast as an Equiv, equivalence between Fin n and Fin m when n = m;
• Fin.castAddEmb m : Fin.castAdd as an Embedding, embed Fin n into Fin (n+m);
• Fin.castSuccEmb : Fin.castSucc as an Embedding, embed Fin n into Fin (n+1);
• Fin.addNatEmb m i : Fin.addNat as an Embedding, add m on i on the right, generalizes Fin.succ;
• Fin.natAddEmb n i : Fin.natAdd as an Embedding, adds n on i on the left;

### Other casts #

• Fin.ofNat': given a positive number n (deduced from [NeZero n]), Fin.ofNat' i is i % n interpreted as an element of Fin n;
• Fin.divNat i : divides i : Fin (m * n) by n;
• Fin.modNat i : takes the mod of i : Fin (m * n) by n;

### Misc definitions #

• Fin.revPerm : Equiv.Perm (Fin n) : Fin.rev as an Equiv.Perm, the antitone involution given by i ↦ n-(i+1)
def finZeroElim {α : Fin 0Sort u_1} (x : Fin 0) :
α x

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

Equations
• = x.elim0
Instances For
instance Fin.instCanLiftNatValLt {n : } :
CanLift (Fin n) Fin.val fun (x : ) => x < n
Equations
• =
def Fin.rec0 {α : Fin 0Sort u_1} (i : Fin 0) :
α i

A dependent variant of Fin.elim0.

Equations
Instances For
theorem Fin.size_positive {n : } :
Fin n0 < 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_of_le_of_lt {n : } {a : Fin n} {b : Fin n} {c : Fin n} :
a bb < ca < c
theorem Fin.lt_of_lt_of_le {n : } {a : Fin n} {b : Fin n} {c : Fin n} :
a < bb ca < c
theorem Fin.le_rfl {n : } {a : Fin n} :
a a
theorem Fin.lt_iff_le_and_ne {n : } {a : Fin n} {b : Fin n} :
a < b a b a b
theorem Fin.lt_or_lt_of_ne {n : } {a : Fin n} {b : Fin n} (h : a b) :
a < b b < a
theorem Fin.lt_or_le {n : } (a : Fin n) (b : Fin n) :
a < b b a
theorem Fin.le_or_lt {n : } (a : Fin n) (b : Fin n) :
a b b < a
theorem Fin.le_of_eq {n : } {a : Fin n} {b : Fin n} (hab : a = b) :
a b
theorem Fin.ge_of_eq {n : } {a : Fin n} {b : Fin n} (hab : a = b) :
b a
theorem Fin.eq_or_lt_of_le {n : } {a : Fin n} {b : Fin n} :
a ba = b a < b
theorem Fin.lt_or_eq_of_le {n : } {a : Fin n} {b : Fin n} :
a ba < b a = b
theorem Fin.lt_last_iff_ne_last {n : } {a : Fin (n + 1)} :
a < a
theorem Fin.ne_zero_of_lt {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (hab : a < b) :
b 0
theorem Fin.ne_last_of_lt {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (hab : a < b) :
a
@[simp]
theorem Fin.equivSubtype_apply {n : } (a : Fin n) :
Fin.equivSubtype a = a,
@[simp]
theorem Fin.equivSubtype_symm_apply {n : } (a : { i : // i < n }) :
Fin.equivSubtype.symm a = a,
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 := }
Instances For

### coercions and constructions #

theorem Fin.val_eq_val {n : } (a : Fin n) (b : Fin n) :
a = b a = b
@[deprecated Fin.ext_iff]
theorem Fin.eq_iff_veq {n : } (a : Fin n) (b : Fin n) :
a = b a = b
theorem Fin.ne_iff_vne {n : } (a : Fin n) (b : Fin n) :
a b a b
@[simp]
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α} :
HEq 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 kFin k'α} {g : Fin lFin l'α} :
HEq 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} :
HEq i j i = j

### order #

theorem Fin.le_iff_val_le_val {n : } {a : Fin n} {b : Fin n} :
a b a b
@[simp]
theorem Fin.val_fin_lt {n : } {a : Fin n} {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 : Fin n} {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
@[simp]
theorem Fin.valEmbedding_apply {n : } (self : Fin n) :
Fin.valEmbedding self = self

The inclusion map Fin n → ℕ is an embedding.

Equations
• Fin.valEmbedding = { toFun := Fin.val, inj' := }
Instances For
@[simp]
theorem Fin.equivSubtype_symm_trans_valEmbedding {n : } :
Fin.equivSubtype.symm.toEmbedding.trans Fin.valEmbedding = Function.Embedding.subtype fun (x : ) => x < 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
def Fin.ofNat'' {n : } [] (i : ) :
Fin n

Given a positive n, Fin.ofNat' i is i % n as an element of Fin n.

Equations
• = i % n,
Instances For
instance Fin.instZeroOfNeZeroNat {n : } [] :
Zero (Fin n)
Equations
• Fin.instZeroOfNeZeroNat = { zero := }
instance Fin.instOneOfNeZeroNat {n : } [] :
One (Fin n)
Equations
• Fin.instOneOfNeZeroNat = { one := }
@[simp]
theorem Fin.val_zero' (n : ) [] :
0 = 0

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

@[simp]
theorem Fin.zero_le' {n : } [] (a : Fin n) :
0 a

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

theorem Fin.pos_iff_ne_zero' {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.revPerm_symm_apply {n : } (i : Fin n) :
(Equiv.symm Fin.revPerm) i = i.rev
@[simp]
theorem Fin.revPerm_apply {n : } (i : Fin n) :
Fin.revPerm i = i.rev
def Fin.revPerm {n : } :

Fin.rev as an Equiv.Perm, the antitone involution Fin n → Fin n given by i ↦ n-(i+1).

Equations
Instances For
@[simp]
theorem Fin.revPerm_symm {n : } :
Equiv.symm Fin.revPerm = Fin.revPerm
theorem Fin.cast_rev {n : } {m : } (i : Fin n) (h : n = m) :
Fin.cast h i.rev = (Fin.cast h i).rev
theorem Fin.rev_eq_iff {n : } {i : Fin n} {j : Fin n} :
i.rev = j i = j.rev
theorem Fin.rev_ne_iff {n : } {i : Fin n} {j : Fin n} :
i.rev j i j.rev
theorem Fin.rev_lt_iff {n : } {i : Fin n} {j : Fin n} :
i.rev < j j.rev < i
theorem Fin.rev_le_iff {n : } {i : Fin n} {j : Fin n} :
i.rev j j.rev i
theorem Fin.lt_rev_iff {n : } {i : Fin n} {j : Fin n} :
i < j.rev j < i.rev
theorem Fin.le_rev_iff {n : } {i : Fin n} {j : Fin n} :
i j.rev j i.rev
@[simp]
theorem Fin.val_rev_zero {n : } [] :
() = n.pred
theorem Fin.last_pos' {n : } [] :
0 <
theorem Fin.one_lt_last {n : } [] :
1 < Fin.last (n + 1)

### addition, numerals, and coercion from Nat #

@[simp]
theorem Fin.val_one' (n : ) [] :
1 = 1 % n
theorem Fin.val_one'' {n : } :
1 = 1 % (n + 1)
instance Fin.nontrivial {n : } :
Nontrivial (Fin (n + 2))
Equations
• =
theorem Fin.add_zero {n : } [] (k : Fin n) :
k + 0 = k
theorem Fin.zero_add {n : } [] (k : Fin n) :
0 + k = k
instance Fin.instOfNatOfNeZeroNat {n : } {a : } [] :
OfNat (Fin n) a
Equations
• Fin.instOfNatOfNeZeroNat = { ofNat := }
instance Fin.inhabited (n : ) [] :
Equations
• = { default := 0 }
instance Fin.inhabitedFinOneAdd (n : ) :
Inhabited (Fin (1 + n))
Equations
• = inferInstance
@[simp]
theorem Fin.default_eq_zero (n : ) [] :
default = 0
@[simp]
theorem Fin.ofNat'_zero {n : } {h : 0 < n} [] :
= 0
@[simp]
theorem Fin.ofNat'_one {n : } {h : 0 < n} [] :
= 1
instance Fin.instNatCast {n : } [] :
Equations
theorem Fin.natCast_def {n : } [] (a : ) :
a = a % n,
theorem Fin.val_add_eq_ite {n : } (a : Fin n) (b : Fin n) :
(a + b) = if n a + b then a + b - n else a + b
@[simp]
theorem Fin.ofNat''_eq_cast (n : ) [] (a : ) :
= a
@[simp]
theorem Fin.val_natCast (a : ) (n : ) [] :
a = a % n
@[deprecated Fin.val_natCast]
theorem Fin.val_nat_cast (a : ) (n : ) [] :
a = a % n

Alias of Fin.val_natCast.

theorem Fin.val_cast_of_lt {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 : } [] (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 : ) [] :
n = 0
@[deprecated Fin.natCast_self]
theorem Fin.nat_cast_self (n : ) [] :
n = 0

Alias of Fin.natCast_self.

@[simp]
theorem Fin.natCast_eq_zero {a : } {n : } [] :
a = 0 n a
@[deprecated Fin.natCast_eq_zero]
theorem Fin.nat_cast_eq_zero {a : } {n : } [] :
a = 0 n a

Alias of Fin.natCast_eq_zero.

@[simp]
theorem Fin.natCast_eq_last (n : ) :
n =
@[deprecated Fin.natCast_eq_last]
theorem Fin.cast_nat_eq_last (n : ) :
n =

Alias of Fin.natCast_eq_last.

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.one_eq_zero_iff {n : } [] :
1 = 0 n = 1
@[simp]
theorem Fin.zero_eq_one_iff {n : } [] :
0 = 1 n = 1

### succ and casts into larger Fin types #

def Fin.succEmb (n : ) :
Fin n Fin (n + 1)

Fin.succ as an Embedding

Equations
• = { toFun := Fin.succ, inj' := }
Instances For
@[simp]
theorem Fin.val_succEmb {n : } :
() = Fin.succ
@[simp]
theorem Fin.exists_succ_eq {n : } {x : Fin (n + 1)} :
(∃ (y : Fin n), y.succ = x) x 0
theorem Fin.exists_succ_eq_of_ne_zero {n : } {x : Fin (n + 1)} (h : x 0) :
∃ (y : Fin n), y.succ = x
@[simp]
theorem Fin.succ_zero_eq_one' {n : } [] :
= 1
theorem Fin.one_pos' {n : } [] :
0 < 1
theorem Fin.zero_ne_one' {n : } [] :
0 1
@[simp]
theorem Fin.succ_one_eq_two' {n : } [] :
= 2

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

@[simp]
theorem Fin.le_zero_iff' {n : } [] {k : Fin n} :
k 0 k = 0

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

@[simp]
theorem Fin.cast_refl {n : } (h : n = n) :
= id
@[simp]
theorem Fin.castLE_inj {n : } {m : } {hmn : m n} {a : Fin m} {b : Fin m} :
Fin.castLE hmn a = Fin.castLE hmn b a = b
@[simp]
theorem Fin.castAdd_inj {n : } {m : } {a : Fin m} {b : Fin m} :
= a = b
theorem Fin.castLE_injective {n : } {m : } (hmn : m n) :
theorem Fin.castAdd_injective (m : ) (n : ) :
@[simp]
theorem Fin.castLEEmb_apply {n : } {m : } (h : n m) (i : Fin n) :
() i =
def Fin.castLEEmb {n : } {m : } (h : n m) :
Fin n Fin m

Fin.castLE as an Embedding, castLEEmb h i embeds i into a larger Fin type.

Equations
• = { toFun := , inj' := }
Instances For
@[simp]
theorem Fin.coe_castLEEmb {m : } {n : } (hmn : m n) :
() = Fin.castLE hmn
theorem Fin.equiv_iff_eq {n : } {m : } :
Nonempty (Fin m Fin n) m = n
@[simp]
theorem Fin.castLE_castSucc {n : } {m : } (i : Fin n) (h : n + 1 m) :
Fin.castLE h i.castSucc =
@[simp]
theorem Fin.castLE_comp_castSucc {n : } {m : } (h : n + 1 m) :
Fin.castSucc =
@[simp]
theorem Fin.castLE_rfl (n : ) :
= id
@[simp]
theorem Fin.range_castLE {n : } {k : } (h : n k) :
= {i : Fin k | i < n}
@[simp]
theorem Fin.coe_of_injective_castLE_symm {n : } {k : } (h : n k) (i : Fin k) (hi : i ) :
(().symm i, hi) = i
theorem Fin.leftInverse_cast {n : } {m : } (eq : n = m) :
theorem Fin.rightInverse_cast {n : } {m : } (eq : n = m) :
theorem Fin.cast_le_cast {n : } {m : } (eq : n = m) {a : Fin n} {b : Fin n} :
Fin.cast eq a Fin.cast eq b a b
@[simp]
theorem finCongr_apply {n : } {m : } (eq : n = m) (i : Fin n) :
(finCongr eq) i = Fin.cast eq i
@[simp]
theorem finCongr_symm_apply {n : } {m : } (eq : n = m) (i : Fin m) :
(finCongr eq).symm i = Fin.cast i
def finCongr {n : } {m : } (eq : n = m) :
Fin n Fin m

The 'identity' equivalence between Fin m and Fin n when m = n.

Equations
• finCongr eq = { toFun := Fin.cast eq, invFun := , left_inv := , right_inv := }
Instances For
@[simp]
theorem finCongr_apply_mk {n : } {m : } (h : m = n) (k : ) (hk : k < m) :
() k, hk = k,
@[simp]
theorem finCongr_refl {n : } (h : optParam (n = n) ) :
@[simp]
theorem finCongr_symm {n : } {m : } (h : m = n) :
().symm =
@[simp]
theorem finCongr_apply_coe {n : } {m : } (h : m = n) (k : Fin m) :
(() k) = k
theorem finCongr_symm_apply_coe {n : } {m : } (h : m = n) (k : Fin n) :
(().symm k) = k
theorem finCongr_eq_equivCast {n : } {m : } (h : n = m) :

While in many cases finCongr is better than Equiv.cast/cast, sometimes we want to apply a generic theorem about cast.

@[simp]
theorem Fin.cast_zero {n : } {n' : } [] {h : n = n'} :
Fin.cast h 0 = 0
theorem Fin.cast_eq_cast {n : } {m : } (h : n = m) :
= cast

While in many cases Fin.cast is better than Equiv.cast/cast, sometimes we want to apply a generic theorem about cast.

@[simp]
theorem Fin.castAddEmb_apply {n : } (m : ) (i : Fin n) :
() i =
def Fin.castAddEmb {n : } (m : ) :
Fin n Fin (n + m)

Fin.castAdd as an Embedding, castAddEmb m i embeds i : Fin n in Fin (n+m). See also Fin.natAddEmb and Fin.addNatEmb.

Equations
Instances For
@[simp]
theorem Fin.castSuccEmb_apply {n : } (i : Fin n) :
Fin.castSuccEmb i =
def Fin.castSuccEmb {n : } :
Fin n Fin (n + 1)

Fin.castSucc as an Embedding, castSuccEmb i embeds i : Fin n in Fin (n+1).

Equations
• Fin.castSuccEmb =
Instances For
@[simp]
theorem Fin.coe_castSuccEmb {n : } :
Fin.castSuccEmb = Fin.castSucc
@[simp]
theorem Fin.castSucc_le_castSucc_iff {n : } {a : Fin n} {b : Fin n} :
a.castSucc b.castSucc a b
@[simp]
theorem Fin.succ_le_castSucc_iff {n : } {a : Fin n} {b : Fin n} :
a.succ b.castSucc a < b
@[simp]
theorem Fin.castSucc_lt_succ_iff {n : } {a : Fin n} {b : Fin n} :
a.castSucc < b.succ a b
theorem Fin.le_of_castSucc_lt_of_succ_lt {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} {i : Fin n} (hl : i.castSucc < a) (hu : b < i.succ) :
b < a
theorem Fin.castSucc_lt_or_lt_succ {n : } (p : Fin (n + 1)) (i : Fin n) :
i.castSucc < p p < i.succ
@[deprecated Fin.castSucc_lt_or_lt_succ]
theorem Fin.succAbove_lt_gt {n : } (p : Fin (n + 1)) (i : Fin n) :
i.castSucc < p p < i.succ

Alias of Fin.castSucc_lt_or_lt_succ.

theorem Fin.succ_le_or_le_castSucc {n : } (p : Fin (n + 1)) (i : Fin n) :
i.succ p p i.castSucc
theorem Fin.exists_castSucc_eq_of_ne_last {n : } {x : Fin (n + 1)} (h : x ) :
∃ (y : Fin n), y.castSucc = x
theorem Fin.forall_fin_succ' {n : } {P : Fin (n + 1)Prop} :
(∀ (i : Fin (n + 1)), P i) (∀ (i : Fin n), P i.castSucc) P ()
theorem Fin.eq_castSucc_or_eq_last {n : } (i : Fin (n + 1)) :
(∃ (j : Fin n), i = j.castSucc) i =
theorem Fin.exists_fin_succ' {n : } {P : Fin (n + 1)Prop} :
(∃ (i : Fin (n + 1)), P i) (∃ (i : Fin n), P i.castSucc) P ()
@[simp]
theorem Fin.castSucc_zero' {n : } [] :

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

theorem Fin.castSucc_pos' {n : } [] {i : Fin n} (h : 0 < i) :
0 < i.castSucc

castSucc i is positive when i is positive.

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

@[simp]
theorem Fin.castSucc_eq_zero_iff' {n : } [] (a : Fin n) :
a.castSucc = 0 a = 0

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

theorem Fin.castSucc_ne_zero_iff' {n : } [] (a : Fin n) :
a.castSucc 0 a 0

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

theorem Fin.castSucc_ne_zero_of_lt {n : } {p : Fin n} {i : Fin n} (h : p < i) :
i.castSucc 0
theorem Fin.succ_ne_last_iff {n : } (a : Fin (n + 1)) :
a.succ Fin.last (n + 1) a
theorem Fin.succ_ne_last_of_lt {n : } {p : Fin n} {i : Fin n} (h : i < p) :
i.succ
@[simp]
theorem Fin.coe_eq_castSucc {n : } {a : Fin n} :
a = a.castSucc
theorem Fin.coe_succ_lt_iff_lt {n : } {j : Fin n} {k : Fin n} :
j < k j < k
@[simp]
theorem Fin.range_castSucc {n : } :
Set.range Fin.castSucc = {i : Fin n.succ | i < n}
@[simp]
theorem Fin.coe_of_injective_castSucc_symm {n : } (i : Fin n.succ) (hi : i Set.range Fin.castSucc) :
((Equiv.ofInjective Fin.castSucc ).symm i, hi) = i
@[simp]
theorem Fin.addNatEmb_apply {n : } (m : ) :
∀ (x : Fin n), () x = x.addNat m
def Fin.addNatEmb {n : } (m : ) :
Fin n Fin (n + m)

Fin.addNat as an Embedding, addNatEmb m i adds m to i, generalizes Fin.succ.

Equations
• = { toFun := fun (x : Fin n) => x.addNat m, inj' := }
Instances For
@[simp]
theorem Fin.natAddEmb_apply (n : ) {m : } (i : Fin m) :
() i =
def Fin.natAddEmb (n : ) {m : } :
Fin m Fin (n + m)

Fin.natAdd as an Embedding, natAddEmb n i adds n to i "on the left".

Equations
• = { toFun := , inj' := }
Instances For

### pred #

theorem Fin.pred_one' {n : } [] (h : optParam (1 0) ) :
Fin.pred 1 h = 0
theorem Fin.pred_last {n : } (h : optParam (¬Fin.last (n + 1) = 0) ) :
(Fin.last (n + 1)).pred h =
theorem Fin.pred_lt_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i 0) :
i.pred hi < j i < j.succ
theorem Fin.lt_pred_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i 0) :
j < i.pred hi j.succ < i
theorem Fin.pred_le_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i 0) :
i.pred hi j i j.succ
theorem Fin.le_pred_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i 0) :
j i.pred hi j.succ i
theorem Fin.castSucc_pred_eq_pred_castSucc {n : } {a : Fin (n + 1)} (ha : a 0) (ha' : optParam (a.castSucc 0) ) :
(a.pred ha).castSucc = a.castSucc.pred ha'
theorem Fin.castSucc_pred_add_one_eq {n : } {a : Fin (n + 1)} (ha : a 0) :
(a.pred ha).castSucc + 1 = a
theorem Fin.le_pred_castSucc_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a.castSucc 0) :
b a.castSucc.pred ha b < a
theorem Fin.pred_castSucc_lt_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a.castSucc 0) :
a.castSucc.pred ha < b a b
theorem Fin.pred_castSucc_lt {n : } {a : Fin (n + 1)} (ha : a.castSucc 0) :
a.castSucc.pred ha < a
theorem Fin.le_castSucc_pred_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a 0) :
b (a.pred ha).castSucc b < a
theorem Fin.castSucc_pred_lt_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a 0) :
(a.pred ha).castSucc < b a b
theorem Fin.castSucc_pred_lt {n : } {a : Fin (n + 1)} (ha : a 0) :
(a.pred ha).castSucc < a
@[inline]
def Fin.castPred {n : } (i : Fin (n + 1)) (h : i ) :
Fin n

castPred i sends i : Fin (n + 1) to Fin n as long as i ≠ last n.

Equations
• i.castPred h = i.castLT
Instances For
@[simp]
theorem Fin.castLT_eq_castPred {n : } (i : Fin (n + 1)) (h : i < ) (h' : optParam (¬i = ) ) :
i.castLT h = i.castPred h'
@[simp]
theorem Fin.coe_castPred {n : } (i : Fin (n + 1)) (h : i ) :
(i.castPred h) = i
@[simp]
theorem Fin.castPred_castSucc {n : } {i : Fin n} (h' : optParam (¬i.castSucc = ) ) :
i.castSucc.castPred h' = i
@[simp]
theorem Fin.castSucc_castPred {n : } (i : Fin (n + 1)) (h : i ) :
(i.castPred h).castSucc = i
theorem Fin.castPred_eq_iff_eq_castSucc {n : } (i : Fin (n + 1)) (hi : i ) (j : Fin n) :
i.castPred hi = j i = j.castSucc
@[simp]
theorem Fin.castPred_mk {n : } (i : ) (h₁ : i < n) (h₂ : optParam (i < n.succ) ) (h₃ : optParam (i, h₂ ) ) :
i, h₂.castPred h₃ = i, h₁
theorem Fin.castPred_le_castPred_iff {n : } {i : Fin (n + 1)} {j : Fin (n + 1)} {hi : i } {hj : j } :
i.castPred hi j.castPred hj i j
theorem Fin.castPred_lt_castPred_iff {n : } {i : Fin (n + 1)} {j : Fin (n + 1)} {hi : i } {hj : j } :
i.castPred hi < j.castPred hj i < j
theorem Fin.castPred_lt_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i ) :
i.castPred hi < j i < j.castSucc
theorem Fin.lt_castPred_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i ) :
j < i.castPred hi j.castSucc < i
theorem Fin.castPred_le_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i ) :
i.castPred hi j i j.castSucc
theorem Fin.le_castPred_iff {n : } {j : Fin n} {i : Fin (n + 1)} (hi : i ) :
j i.castPred hi j.castSucc i
theorem Fin.castPred_inj {n : } {i : Fin (n + 1)} {j : Fin (n + 1)} {hi : i } {hj : j } :
i.castPred hi = j.castPred hj i = j
theorem Fin.castPred_zero' {n : } [] (h : optParam (¬0 = ) ) :
= 0
theorem Fin.castPred_zero {n : } (h : optParam (¬0 = Fin.last (n + 1)) ) :
= 0
@[simp]
theorem Fin.castPred_one {n : } [] (h : optParam (¬1 = Fin.last (n + 1)) ) :
= 1
theorem Fin.rev_pred {n : } {i : Fin (n + 1)} (h : i 0) (h' : optParam (i.rev ) ) :
(i.pred h).rev = i.rev.castPred h'
theorem Fin.rev_castPred {n : } {i : Fin (n + 1)} (h : i ) (h' : optParam (i.rev 0) ) :
(i.castPred h).rev = i.rev.pred h'
theorem Fin.succ_castPred_eq_castPred_succ {n : } {a : Fin (n + 1)} (ha : a ) (ha' : optParam (a.succ Fin.last (n + 1)) ) :
(a.castPred ha).succ = a.succ.castPred ha'
theorem Fin.succ_castPred_eq_add_one {n : } {a : Fin (n + 1)} (ha : a ) :
(a.castPred ha).succ = a + 1
theorem Fin.castpred_succ_le_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a.succ Fin.last (n + 1)) :
a.succ.castPred ha b a < b
theorem Fin.lt_castPred_succ_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a.succ Fin.last (n + 1)) :
b < a.succ.castPred ha b a
theorem Fin.lt_castPred_succ {n : } {a : Fin (n + 1)} (ha : a.succ Fin.last (n + 1)) :
a < a.succ.castPred ha
theorem Fin.succ_castPred_le_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a ) :
(a.castPred ha).succ b a < b
theorem Fin.lt_succ_castPred_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a ) :
b < (a.castPred ha).succ b a
theorem Fin.lt_succ_castPred {n : } {a : Fin (n + 1)} (ha : a ) :
a < (a.castPred ha).succ
theorem Fin.castPred_le_pred_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a ) (hb : b 0) :
a.castPred ha b.pred hb a < b
theorem Fin.pred_lt_castPred_iff {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a 0) (hb : b ) :
a.pred ha < b.castPred hb a b
theorem Fin.pred_lt_castPred {n : } {a : Fin (n + 1)} (h₁ : a 0) (h₂ : a ) :
a.pred h₁ < a.castPred h₂
def Fin.succAbove {n : } (p : Fin (n + 1)) (i : Fin n) :
Fin (n + 1)

succAbove p i embeds Fin n into Fin (n + 1) with a hole around p.

Equations
• p.succAbove i = if i.castSucc < p then i.castSucc else i.succ
Instances For
theorem Fin.succAbove_of_castSucc_lt {n : } (p : Fin (n + 1)) (i : Fin n) (h : i.castSucc < p) :
p.succAbove i = i.castSucc

Embedding i : Fin n into Fin (n + 1) with a hole around p : Fin (n + 1) embeds i by castSucc when the resulting i.castSucc < p.

theorem Fin.succAbove_of_succ_le {n : } (p : Fin (n + 1)) (i : Fin n) (h : i.succ p) :
p.succAbove i = i.castSucc
theorem Fin.succAbove_of_le_castSucc {n : } (p : Fin (n + 1)) (i : Fin n) (h : p i.castSucc) :
p.succAbove i = i.succ

Embedding i : Fin n into Fin (n + 1) with a hole around p : Fin (n + 1) embeds i by succ when the resulting p < i.succ.

theorem Fin.succAbove_of_lt_succ {n : } (p : Fin (n + 1)) (i : Fin n) (h : p < i.succ) :
p.succAbove i = i.succ
theorem Fin.succAbove_succ_of_lt {n : } (p : Fin n) (i : Fin n) (h : p < i) :
p.succ.succAbove i = i.succ
theorem Fin.succAbove_succ_of_le {n : } (p : Fin n) (i : Fin n) (h : i p) :
p.succ.succAbove i = i.castSucc
@[simp]
theorem Fin.succAbove_succ_self {n : } (j : Fin n) :
j.succ.succAbove j = j.castSucc
theorem Fin.succAbove_castSucc_of_lt {n : } (p : Fin n) (i : Fin n) (h : i < p) :
p.castSucc.succAbove i = i.castSucc
theorem Fin.succAbove_castSucc_of_le {n : } (p : Fin n) (i : Fin n) (h : p i) :
p.castSucc.succAbove i = i.succ
@[simp]
theorem Fin.succAbove_castSucc_self {n : } (j : Fin n) :
j.castSucc.succAbove j = j.succ
theorem Fin.succAbove_pred_of_lt {n : } (p : Fin (n + 1)) (i : Fin (n + 1)) (h : p < i) (hi : optParam (i 0) ) :
p.succAbove (i.pred hi) = i
theorem Fin.succAbove_pred_of_le {n : } (p : Fin (n + 1)) (i : Fin (n + 1)) (h : i p) (hi : i 0) :
p.succAbove (i.pred hi) = (i.pred hi).castSucc
@[simp]
theorem Fin.succAbove_pred_self {n : } (p : Fin (n + 1)) (h : p 0) :
p.succAbove (p.pred h) = (p.pred h).castSucc
theorem Fin.succAbove_castPred_of_lt {n : } (p : Fin (n + 1)) (i : Fin (n + 1)) (h : i < p) (hi : optParam (i ) ) :
p.succAbove (i.castPred hi) = i
theorem Fin.succAbove_castPred_of_le {n : } (p : Fin (n + 1)) (i : Fin (n + 1)) (h : p i) (hi : i ) :
p.succAbove (i.castPred hi) = (i.castPred hi).succ
theorem Fin.succAbove_castPred_self {n : } (p : Fin (n + 1)) (h : p ) :
p.succAbove (p.castPred h) = (p.castPred h).succ
theorem Fin.succAbove_rev_left {n : } (p : Fin (n + 1)) (i : Fin n) :
p.rev.succAbove i = (p.succAbove i.rev).rev
theorem Fin.succAbove_rev_right {n : } (p : Fin (n + 1)) (i : Fin n) :
p.succAbove i.rev = (p.rev.succAbove i).rev
theorem Fin.succAbove_ne {n : } (p : Fin (n + 1)) (i : Fin n) :
p.succAbove i p

Embedding i : Fin n into Fin (n + 1) with a hole around p : Fin (n + 1) never results in p itself

theorem Fin.ne_succAbove {n : } (p : Fin (n + 1)) (i : Fin n) :
p p.succAbove i
theorem Fin.succAbove_right_injective {n : } {p : Fin (n + 1)} :
Function.Injective p.succAbove

Given a fixed pivot p : Fin (n + 1), p.succAbove is injective.

theorem Fin.succAbove_right_inj {n : } {p : Fin (n + 1)} {i : Fin n} {j : Fin n} :
p.succAbove i = p.succAbove j i = j

Given a fixed pivot p : Fin (n + 1), p.succAbove is injective.

@[simp]
theorem Fin.succAboveEmb_apply {n : } (p : Fin (n + 1)) (i : Fin n) :
p.succAboveEmb i = p.succAbove i
def Fin.succAboveEmb {n : } (p : Fin (n + 1)) :
Fin n Fin (n + 1)

Fin.succAbove p as an Embedding.

Equations
• p.succAboveEmb = { toFun := p.succAbove, inj' := }
Instances For
@[simp]
theorem Fin.coe_succAboveEmb {n : } (p : Fin (n + 1)) :
p.succAboveEmb = p.succAbove
@[simp]
theorem Fin.succAbove_ne_zero_zero {n : } [] {a : Fin (n + 1)} (ha : a 0) :
a.succAbove 0 = 0
theorem Fin.succAbove_eq_zero_iff {n : } [] {a : Fin (n + 1)} {b : Fin n} (ha : a 0) :
a.succAbove b = 0 b = 0
theorem Fin.succAbove_ne_zero {n : } [] {a : Fin (n + 1)} {b : Fin n} (ha : a 0) (hb : b 0) :
a.succAbove b 0
@[simp]
theorem Fin.succAbove_zero {n : } :
= Fin.succ

Embedding Fin n into Fin (n + 1) with a hole around zero embeds by succ.

theorem Fin.succAbove_zero_apply {n : } (i : Fin n) :
= i.succ
@[simp]
theorem Fin.succAbove_ne_last_last {n : } {a : Fin (n + 2)} (h : a Fin.last (n + 1)) :
a.succAbove () = Fin.last (n + 1)
theorem Fin.succAbove_eq_last_iff {n : } {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a Fin.last (n + 1)) :
a.succAbove b = Fin.last (n + 1) b =
theorem Fin.succAbove_ne_last {n : } {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a Fin.last (n + 1)) (hb : b ) :
a.succAbove b Fin.last (n + 1)
@[simp]
theorem Fin.succAbove_last {n : } :
().succAbove = Fin.castSucc

Embedding Fin n into Fin (n + 1) with a hole around last n embeds by castSucc.

theorem Fin.succAbove_last_apply {n : } (i : Fin n) :
().succAbove i = i.castSucc
@[deprecated]
theorem Fin.succAbove_lt_ge {n : } (p : Fin (n + 1)) (i : Fin n) :
i.castSucc < p p i.castSucc
theorem Fin.succAbove_lt_iff_castSucc_lt {n : } (p : Fin (n + 1)) (i : Fin n) :
p.succAbove i < p i.castSucc < p

Embedding i : Fin n into Fin (n + 1) using a pivot p that is greater results in a value that is less than p.

theorem Fin.succAbove_lt_iff_succ_le {n : } (p : Fin (n + 1)) (i : Fin n) :
p.succAbove i < p i.succ p
theorem Fin.lt_succAbove_iff_le_castSucc {n : } (p : Fin (n + 1)) (i : Fin n) :
p < p.succAbove i p i.castSucc

Embedding i : Fin n into Fin (n + 1) using a pivot p that is lesser results in a value that is greater than p.

theorem Fin.lt_succAbove_iff_lt_castSucc {n : } (p : Fin (n + 1)) (i : Fin n) :
p < p.succAbove i p < i.succ
theorem Fin.succAbove_pos {n : } [] (p : Fin (n + 1)) (i : Fin n) (h : 0 < i) :
0 < p.succAbove i

Embedding a positive Fin n results in a positive Fin (n + 1)

theorem Fin.castPred_succAbove {n : } (x : Fin n) (y : Fin (n + 1)) (h : x.castSucc < y) (h' : optParam (y.succAbove x ) ) :
(y.succAbove x).castPred h' = x
theorem Fin.pred_succAbove {n : } (x : Fin n) (y : Fin (n + 1)) (h : y x.castSucc) (h' : optParam (y.succAbove x 0) ) :
(y.succAbove x).pred h' = x
theorem Fin.exists_succAbove_eq {n : } {x : Fin (n + 1)} {y : Fin (n + 1)} (h : x y) :
∃ (z : Fin n), y.succAbove z = x
@[simp]
theorem Fin.exists_succAbove_eq_iff {n : } {x : Fin (n + 1)} {y : Fin (n + 1)} :
(∃ (z : Fin n), x.succAbove z = y) y x
@[simp]
theorem Fin.range_succAbove {n : } (p : Fin (n + 1)) :
Set.range p.succAbove = {p}

The range of p.succAbove is everything except p.

@[simp]
theorem Fin.range_succ (n : ) :
Set.range Fin.succ = {0}

succAbove is injective at the pivot

@[simp]
theorem Fin.succAbove_left_inj {n : } {x : Fin (n + 1)} {y : Fin (n + 1)} :
x.succAbove = y.succAbove x = y

succAbove is injective at the pivot

@[simp]
theorem Fin.zero_succAbove {n : } (i : Fin n) :
= i.succ
@[simp]
theorem Fin.succ_succAbove_zero {n : } [] (i : Fin n) :
i.succ.succAbove 0 = 0
@[simp]
theorem Fin.succ_succAbove_succ {n : } (i : Fin (n + 1)) (j : Fin n) :
i.succ.succAbove j.succ = (i.succAbove j).succ

succ commutes with succAbove.

@[simp]
theorem Fin.castSucc_succAbove_castSucc {n : } {i : Fin (n + 1)} {j : Fin n} :
i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

castSucc commutes with succAbove.

theorem Fin.pred_succAbove_pred {n : } {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a 0) (hb : b 0) (hk : optParam (a.succAbove b 0) ) :
(a.pred ha).succAbove (b.pred hb) = (a.succAbove b).pred hk

pred commutes with succAbove.

theorem Fin.castPred_succAbove_castPred {n : } {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a Fin.last (n + 1)) (hb : b ) (hk : optParam (a.succAbove b Fin.last (n + 1)) ) :
(a.castPred ha).succAbove (b.castPred hb) = (a.succAbove b).castPred hk

castPred commutes with succAbove.

theorem Fin.rev_succAbove {n : } (p : Fin (n + 1)) (i : Fin n) :
(p.succAbove i).rev = p.rev.succAbove i.rev

rev commutes with succAbove.

@[simp]
theorem Fin.succ_succAbove_one {n : } [] (i : Fin (n + 1)) :
i.succ.succAbove 1 = (i.succAbove 0).succ

By moving succ to the outside of this expression, we create opportunities for further simplification using succAbove_zero or succ_succAbove_zero.

@[simp]
theorem Fin.one_succAbove_succ {n : } (j : Fin n) :
Fin.succAbove 1 j.succ = j.succ.succ
@[simp]
theorem Fin.one_succAbove_one {n : } :
= 2
def Fin.predAbove {n : } (p : Fin n) (i : Fin (n + 1)) :
Fin n

predAbove p i surjects i : Fin (n+1) into Fin n by subtracting one if p < i.

Equations
• p.predAbove i = if h : p.castSucc < i then i.pred else i.castPred
Instances For
theorem Fin.predAbove_of_le_castSucc {n : } (p : Fin n) (i : Fin (n + 1)) (h : i p.castSucc) (hi : optParam (i ) ) :
p.predAbove i = i.castPred hi
theorem Fin.predAbove_of_lt_succ {n : } (p : Fin n) (i : Fin (n + 1)) (h : i < p.succ) (hi : optParam (i ) ) :
p.predAbove i = i.castPred hi
theorem Fin.predAbove_of_castSucc_lt {n : } (p : Fin n) (i : Fin (n + 1)) (h : p.castSucc < i) (hi : optParam (i 0) ) :
p.predAbove i = i.pred hi
theorem Fin.predAbove_of_succ_le {n : } (p : Fin n) (i : Fin (n + 1)) (h : p.succ i) (hi : optParam (i 0) ) :
p.predAbove i = i.pred hi
theorem Fin.predAbove_succ_of_lt {n : } (p : Fin n) (i : Fin n) (h : i < p) (hi : optParam (i.succ ) ) :
p.predAbove i.succ = i.succ.castPred hi
theorem Fin.predAbove_succ_of_le {n : } (p : Fin n) (i : Fin n) (h : p i) :
p.predAbove i.succ = i
@[simp]
theorem Fin.predAbove_succ_self {n : } (p : Fin n) :
p.predAbove p.succ = p
theorem Fin.predAbove_castSucc_of_lt {n : } (p : Fin n) (i : Fin n) (h : p < i) (hi : optParam (i.castSucc 0) ) :
p.predAbove i.castSucc = i.castSucc.pred hi
theorem Fin.predAbove_castSucc_of_le {n : } (p : Fin n) (i : Fin n) (h : i p) :
p.predAbove i.castSucc = i
@[simp]
theorem Fin.predAbove_castSucc_self {n : } (p : Fin n) :
p.predAbove p.castSucc = p
theorem Fin.predAbove_pred_of_lt {n : } (p : Fin (n + 1)) (i : Fin (n + 1)) (h : i < p) (hp : optParam (p 0) ) (hi : optParam (i ) ) :
(p.pred hp).predAbove i = i.castPred hi
theorem Fin.predAbove_pred_of_le {n : } (p : Fin (n + 1)) (i : Fin (n + 1)) (h : p i) (hp : p 0) (hi : optParam (i 0) ) :
(p.pred hp).predAbove i = i.pred hi
theorem Fin.predAbove_pred_self {n : } (p : Fin (n + 1)) (hp : p 0) :
(p.pred hp).predAbove p = p.pred hp
theorem Fin.predAbove_castPred_of_lt {n : } (p : Fin (n + 1)) (i : Fin (n + 1)) (h : p < i) (hp : optParam (p ) ) (hi : optParam (i 0) ) :
(p.castPred hp).predAbove i = i.pred hi
theorem Fin.predAbove_castPred_of_le {n : } (p : Fin (n + 1)) (i : Fin (n + 1)) (h : i p) (hp : p ) (hi : optParam (i ) ) :
(p.castPred hp).predAbove i = i.castPred hi
theorem Fin.predAbove_castPred_self {n : } (p : Fin (n + 1)) (hp : p ) :
(p.castPred hp).predAbove p = p.castPred hp
theorem Fin.predAbove_rev_left {n : } (p : Fin n) (i : Fin (n + 1)) :
p.rev.predAbove i = (p.predAbove i.rev).rev
theorem Fin.predAbove_rev_right {n : } (p : Fin n) (i : Fin (n + 1)) :
p.predAbove i.rev = (p.rev.predAbove i).rev
@[simp]
theorem Fin.predAbove_right_zero {n : } [] {i : Fin n} :
i.predAbove 0 = 0
@[simp]
theorem Fin.predAbove_zero_succ {n : } [] {i : Fin n} :
Fin.predAbove 0 i.succ = i
@[simp]
theorem Fin.succ_predAbove_zero {n : } [] {j : Fin (n + 1)} (h : j 0) :
().succ = j
@[simp]
theorem Fin.predAbove_zero_of_ne_zero {n : } [] {i : Fin (n + 1)} (hi : i 0) :
= i.pred hi
theorem Fin.predAbove_zero {n : } [] {i : Fin (n + 1)} :
= if hi : i = 0 then 0 else i.pred hi
@[simp]
theorem Fin.predAbove_right_last {n : } {i : Fin (n + 1)} :
i.predAbove (Fin.last (n + 1)) =
@[simp]
theorem Fin.predAbove_last_castSucc {n : } {i : Fin (n + 1)} :
().predAbove i.castSucc = i
@[simp]
theorem Fin.predAbove_last_of_ne_last {n : } {i : Fin (n + 2)} (hi : i Fin.last (n + 1)) :
().predAbove i = i.castPred hi
theorem Fin.predAbove_last_apply {n : } {i : Fin (n + 2)} :
().predAbove i = if hi : i = Fin.last (n + 1) then else i.castPred hi
@[simp]
theorem Fin.succAbove_predAbove {n : } {p : Fin n} {i : Fin (n + 1)} (h : i p.castSucc) :
p.castSucc.succAbove (p.predAbove i) = i

Sending Fin (n+1) to Fin n by subtracting one from anything above p then back to Fin (n+1) with a gap around p is the identity away from p.

@[simp]
theorem Fin.predAbove_succAbove {n : } (p : Fin n) (i : Fin n) :
p.predAbove (p.castSucc.succAbove i) = i

Sending Fin n into Fin (n + 1) with a gap at p then back to Fin n by subtracting one from anything above p is the identity.

@[simp]
theorem Fin.succ_predAbove_succ {n : } (a : Fin n) (b : Fin (n + 1)) :
a.succ.predAbove b.succ = (a.predAbove b).succ

succ commutes with predAbove.

@[simp]
theorem Fin.castSucc_predAbove_castSucc {n : } (a : Fin n) (b : Fin (n + 1)) :
a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

castSucc commutes with predAbove.

theorem Fin.rev_predAbove {n : } (p : Fin n) (i : Fin (n + 1)) :
(p.predAbove i).rev = p.rev.predAbove i.rev

rev commutes with predAbove.

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,
Instances For
@[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,
Instances For
@[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)α} :
((fun (x x_1 : Fin (n + 1)) => x < x_1) r) f f ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
instance Fin.neg (n : ) :
Neg (Fin n)

Negation on Fin n

Equations
• = { neg := fun (a : Fin n) => (n - a) % n, }
theorem Fin.neg_def {n : } (a : Fin n) :
-a = (n - a) % n,
theorem Fin.coe_neg {n : } (a : Fin n) :
(-a) = (n - a) % n
theorem Fin.eq_zero (n : Fin 1) :
n = 0
Equations
@[simp]
theorem Fin.coe_fin_one (a : Fin 1) :
a = 0
theorem Fin.eq_one_of_neq_zero (i : Fin 2) (hi : i 0) :
i = 1
@[simp]
theorem Fin.coe_neg_one {n : } :
(-1) = n
theorem Fin.last_sub {n : } (i : Fin (n + 1)) :
- i = i.rev
theorem Fin.add_one_le_of_lt {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (h : a < b) :
a + 1 b
theorem Fin.exists_eq_add_of_le {n : } {a : Fin n} {b : Fin n} (h : a b) :
kb, b = a + k
theorem Fin.exists_eq_add_of_lt {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} (h : a < b) :
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
@[simp]
theorem Fin.coe_ofNat_eq_mod (m : ) (n : ) [] :
n = n % m

### mul #

theorem Fin.mul_one' {n : } [] (k : Fin n) :
k * 1 = k
theorem Fin.one_mul' {n : } [] (k : Fin n) :
1 * k = k
theorem Fin.mul_zero' {n : } [] (k : Fin n) :
k * 0 = 0
theorem Fin.zero_mul' {n : } [] (k : Fin n) :
0 * k = 0
instance Fin.toExpr (n : ) :
Equations
• One or more equations did not get rendered due to their size.