# Documentation

Mathlib.Data.Fin.Basic

# 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.succAbove_cases: 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

### Order embeddings and an order isomorphism #

• Fin.orderIsoSubtype : coercion to { i // i < n } as an OrderIso;
• Fin.valEmbedding : coercion to natural numbers as an Embedding;
• Fin.valOrderEmbedding : coercion to natural numbers as an OrderEmbedding;
• Fin.succEmbedding : Fin.succ as an OrderEmbedding;
• Fin.castLe h : embed Fin n into Fin m, h : n ≤ m;
• Fin.cast : order isomorphism between Fin n and Fin m provided that n = m, see also Equiv.finCongr;
• Fin.castAdd m : embed Fin n into Fin (n+m);
• Fin.castSucc : embed Fin n into Fin (n+1);
• Fin.succAbove p : embed Fin n into Fin (n + 1) with a hole around p;
• Fin.addNat m i : add m on i on the right, generalizes Fin.succ;
• Fin.natAdd n i 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.castLt i h : embed i into a Fin where h proves it belongs into;
• Fin.predAbove (p : Fin n) i : embed i : Fin (n+1) into Fin n by subtracting one if p < i;
• Fin.castPred : embed Fin (n + 2) into Fin (n + 1) by mapping Fin.last (n + 1) to Fin.last n;
• Fin.subNat i h : subtract m from i ≥ m, generalizes Fin.pred;
• Fin.clamp n m : min n m as an element of Fin (m + 1);
• 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.last n : The greatest value of Fin (n+1).
• Fin.rev : Fin n → Fin n : 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
def Fin.elim0' {α : Sort u_1} (x : Fin 0) :
α

A non-dependent variant of elim0.

Equations
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.mod_def {n : } (a : Fin n) (m : Fin n) :
a % m = { val := a % m % n, isLt := (_ : a % m % n < n) }
theorem Fin.add_def {n : } (a : Fin n) (b : Fin n) :
a + b = { val := (a + b) % n, isLt := (_ : (a + b) % n < n) }
theorem Fin.mul_def {n : } (a : Fin n) (b : Fin n) :
a * b = { val := a * b % n, isLt := (_ : a * b % n < n) }
theorem Fin.sub_def {n : } (a : Fin n) (b : Fin n) :
a - b = { val := (a + (n - b)) % n, isLt := (_ : (a + (n - b)) % n < n) }
theorem Fin.size_positive' {n : } [inst : Nonempty (Fin n)] :
0 < n
theorem Fin.prop {n : } (a : Fin n) :
a < n
@[simp]
theorem Fin.is_lt {n : } (a : Fin n) :
a < n
theorem Fin.pos {n : } (i : Fin n) :
0 < n
@[simp]
theorem Fin.equivSubtype_symm_apply {n : } (a : { i // i < n }) :
↑(Equiv.symm Fin.equivSubtype) a = { val := a, isLt := (_ : a < n) }
@[simp]
theorem Fin.equivSubtype_apply {n : } (a : Fin n) :
Fin.equivSubtype a = { val := a, property := (_ : a < n) }
def Fin.equivSubtype {n : } :
Fin n { i // i < n }

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

Equations
• One or more equations did not get rendered due to their size.

### coercions and constructions #

@[simp]
theorem Fin.eta {n : } (a : Fin n) (h : a < n) :
{ val := a, isLt := h } = a
theorem Fin.ext {n : } {a : Fin n} {b : Fin n} (h : a = b) :
a = b
theorem Fin.ext_iff {n : } {a : Fin n} {b : Fin n} :
a = b a = b
theorem Fin.val_eq_val {n : } (a : Fin n) (b : Fin n) :
a = b a = b
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} :
{ val := a, isLt := h } = { val := a', isLt := h' } a = a'
theorem Fin.mk.inj_iff {n : } {a : } {b : } {ha : a < n} {hb : b < n} :
{ val := a, isLt := ha } = { val := b, isLt := hb } a = b
theorem Fin.val_mk {m : } {n : } (h : m < n) :
{ val := m, isLt := h } = m
theorem Fin.eq_mk_iff_val_eq {n : } {a : Fin n} {k : } {hk : k < n} :
a = { val := k, isLt := hk } a = k
theorem Fin.mk_val {n : } (i : Fin n) :
{ val := i, isLt := (_ : i < n) } = i
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 { val := i, isLt := (_ : i < l) }

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_ext_iff {k : } {l : } (h : k = l) {i : Fin k} {j : Fin l} :
HEq i j i = j
theorem Fin.exists_iff {n : } {p : Fin nProp} :
(i, p i) i h, p { val := i, isLt := h }
theorem Fin.forall_iff {n : } {p : Fin nProp} :
((i : Fin n) → p i) (i : ) → (h : i < n) → p { val := i, isLt := h }

### order #

theorem Fin.is_le {n : } (i : Fin (n + 1)) :
i n
@[simp]
theorem Fin.is_le' {n : } {a : Fin n} :
a n
theorem Fin.lt_iff_val_lt_val {n : } {a : Fin n} {b : Fin n} :
a < b a < b
theorem Fin.le_iff_val_le_val {n : } {a : Fin n} {b : Fin n} :
a b a b
theorem Fin.mk_lt_of_lt_val {n : } {b : Fin n} {a : } (h : a < b) :
{ val := a, isLt := (_ : a < n) } < b
theorem Fin.mk_le_of_le_val {n : } {b : Fin n} {a : } (h : a b) :
{ val := a, isLt := (_ : a < n) } 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.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Fin.mk_le_mk {n : } {x : } {y : } {hx : x < n} {hy : y < n} :
{ val := x, isLt := hx } { val := y, isLt := hy } x y
@[simp]
theorem Fin.mk_lt_mk {n : } {x : } {y : } {hx : x < n} {hy : y < n} :
{ val := x, isLt := hx } < { val := y, isLt := hy } x < y
theorem Fin.min_val {n : } {a : Fin n} :
min (a) n = a
theorem Fin.max_val {n : } {a : Fin n} :
max (a) n = n
Equations
• Fin.instPartialOrderFin = inferInstance
@[simp]
theorem Fin.orderIsoSubtype_apply {n : } (a : Fin n) :
(RelIso.toRelEmbedding Fin.orderIsoSubtype).toEmbedding a = { val := a, property := (_ : a < n) }
@[simp]
theorem Fin.orderIsoSubtype_symm_apply {n : } (a : { i // i < n }) :
(RelIso.toRelEmbedding (RelIso.symm Fin.orderIsoSubtype)).toEmbedding a = { val := a, isLt := (_ : a < n) }
def Fin.orderIsoSubtype {n : } :
Fin n ≃o { i // i < n }

The equivalence Fin n ≃ { i // i < n } is an order isomorphism.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Fin.valEmbedding_apply {n : } (self : Fin n) :
Fin.valEmbedding self = self

The inclusion map Fin n → ℕ is an embedding.

Equations
@[simp]
theorem Fin.valOrderEmbedding_apply (n : ) (self : Fin n) :
().toEmbedding self = self

The inclusion map Fin n → ℕ is an order embedding.

Equations
• = { toEmbedding := Fin.valEmbedding, map_rel_iff' := (_ : ∀ {a b : Fin n}, Fin.valEmbedding a Fin.valEmbedding b Fin.valEmbedding a Fin.valEmbedding b) }
instance Fin.Lt.isWellOrder (n : ) :
IsWellOrder (Fin n) fun x x_1 => x < x_1

The ordering on Fin n is a well order.

Equations

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.instWellFoundedRelationFin = measure Fin.val
def Fin.ofNat'' {n : } [inst : ] (i : ) :
Fin n

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

Equations
• = { val := i % n, isLt := (_ : i % n < n) }
instance Fin.instZeroFin {n : } [inst : ] :
Zero (Fin n)
Equations
• Fin.instZeroFin = { zero := }
instance Fin.instOneFin {n : } [inst : ] :
One (Fin n)
Equations
• Fin.instOneFin = { one := }
@[simp]
theorem Fin.val_zero (n : ) [inst : ] :
0 = 0
@[simp]
theorem Fin.mk_zero {n : } [inst : ] :
{ val := 0, isLt := (_ : 0 < n) } = 0
@[simp]
theorem Fin.zero_le {n : } [inst : ] (a : Fin n) :
0 a
theorem Fin.zero_lt_one {n : } :
0 < 1
@[simp]
theorem Fin.not_lt_zero {n : } (a : Fin ()) :
¬a < 0
theorem Fin.pos_iff_ne_zero {n : } [inst : ] (a : Fin n) :
0 < a a 0
theorem Fin.eq_zero_or_eq_succ {n : } (i : Fin (n + 1)) :
i = 0 j, i =
theorem Fin.eq_succ_of_ne_zero {n : } {i : Fin (n + 1)} (hi : i 0) :
j, i =
def Fin.rev {n : } :

The antitone involution Fin n → Fin n given by i ↦ n-(i+1).

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Fin.val_rev {n : } (i : Fin n) :
↑(Fin.rev i) = n - (i + 1)
theorem Fin.rev_inj {n : } {i : Fin n} {j : Fin n} :
Fin.rev i = Fin.rev j i = j
@[simp]
theorem Fin.rev_rev {n : } (i : Fin n) :
Fin.rev (Fin.rev i) = i
@[simp]
theorem Fin.rev_symm {n : } :
Equiv.symm Fin.rev = Fin.rev
theorem Fin.rev_eq {n : } {a : } (i : Fin (n + 1)) (h : n = a + i) :
Fin.rev i = { val := a, isLt := (_ : a < ) }
@[simp]
theorem Fin.rev_le_rev {n : } {i : Fin n} {j : Fin n} :
Fin.rev i Fin.rev j j i
@[simp]
theorem Fin.rev_lt_rev {n : } {i : Fin n} {j : Fin n} :
Fin.rev i < Fin.rev j j < i
@[simp]
theorem Fin.revOrderIso_apply {n : } :
∀ (a : (Fin n)ᵒᵈ), (RelIso.toRelEmbedding Fin.revOrderIso).toEmbedding a = Fin.rev (OrderDual.ofDual a)
@[simp]
theorem Fin.revOrderIso_toEquiv {n : } :
Fin.revOrderIso.toEquiv = Equiv.trans OrderDual.ofDual Fin.rev

Fin.rev n as an order-reversing isomorphism.

Equations
• Fin.revOrderIso = { toEquiv := Equiv.trans OrderDual.ofDual Fin.rev, map_rel_iff' := (_ : ∀ {a b : (Fin n)ᵒᵈ}, Fin.rev a Fin.rev b b a) }
@[simp]
theorem Fin.revOrderIso_symm_apply {n : } (i : Fin n) :
(RelIso.toRelEmbedding (OrderIso.symm Fin.revOrderIso)).toEmbedding i = OrderDual.toDual (Fin.rev i)
def Fin.last (n : ) :
Fin (n + 1)

The greatest value of Fin (n+1)

Equations
• = { val := n, isLt := (_ : n < ) }
@[simp]
theorem Fin.val_last (n : ) :
↑() = n
theorem Fin.le_last {n : } (i : Fin (n + 1)) :
i
Equations
Equations
theorem Fin.last_pos {n : } :
0 < Fin.last (n + 1)
theorem Fin.eq_last_of_not_lt {n : } {i : Fin (n + 1)} (h : ¬i < n) :
i =
theorem Fin.val_lt_last {n : } {i : Fin (n + 1)} (h : i ) :
i < n
@[simp]
theorem Fin.coe_orderIso_apply {n : } {m : } (e : Fin n ≃o Fin m) (i : Fin n) :
↑(().toEmbedding i) = i

If e is an orderIso between Fin n and Fin m, then n = m and e is the identity map. In this lemma we state that for each i : Fin n we have (e i : ℕ) = (i : ℕ).

instance Fin.orderIso_subsingleton {n : } {α : Type u_1} [inst : ] :
Equations
instance Fin.orderIso_subsingleton' {n : } {α : Type u_1} [inst : ] :
Equations
instance Fin.orderIsoUnique {n : } :
Equations
theorem Fin.strictMono_unique {n : } {α : Type u_1} [inst : ] {f : Fin nα} {g : Fin nα} (hf : ) (hg : ) (h : ) :
f = g

Two strictly monotone functions from Fin n are equal provided that their ranges are equal.

theorem Fin.orderEmbedding_eq {n : } {α : Type u_1} [inst : ] {f : Fin n ↪o α} {g : Fin n ↪o α} (h : Set.range f.toEmbedding = Set.range g.toEmbedding) :
f = g

Two order embeddings of Fin n are equal provided that their ranges are equal.

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

@[simp]
theorem Fin.val_one (n : ) :
1 = 1
@[simp]
theorem Fin.val_one' (n : ) [inst : ] :
1 = 1 % n
theorem Fin.val_one'' {n : } :
1 = 1 % (n + 1)
@[simp]
theorem Fin.mk_one {n : } :
{ val := 1, isLt := (_ : < Nat.succ (n + 1)) } = 1
instance Fin.nontrivial {n : } :
Nontrivial (Fin (n + 2))
Equations
theorem Fin.add_zero {n : } [inst : ] (k : Fin n) :
k + 0 = k
theorem Fin.zero_add {n : } [inst : ] (k : Fin n) :
0 + k = k
instance Fin.instOfNatFin {n : } {a : } [inst : ] :
OfNat (Fin n) a
Equations
@[simp]
theorem Fin.ofNat'_zero {n : } {h : n > 0} [inst : ] :
= 0
@[simp]
theorem Fin.ofNat'_one {n : } {h : n > 0} [inst : ] :
= 1
Equations
instance Fin.addCommMonoid (n : ) [inst : ] :
Equations
instance Fin.instAddMonoidWithOneFin (n : ) [inst : ] :
Equations
• = let src := ; AddMonoidWithOne.mk
theorem Fin.val_add {n : } (a : Fin n) (b : Fin n) :
↑(a + b) = (a + b) % 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
theorem Fin.val_bit0 {n : } (k : Fin n) :
↑(bit0 k) = bit0 k % n
theorem Fin.val_bit1 {n : } [inst : ] (k : Fin n) :
↑(bit1 k) = bit1 k % n
theorem Fin.val_add_one_of_lt {n : } {i : Fin ()} (h : i < ) :
↑(i + 1) = i + 1
@[simp]
theorem Fin.last_add_one (n : ) :
+ 1 = 0
theorem Fin.val_add_one {n : } (i : Fin (n + 1)) :
↑(i + 1) = if i = then 0 else i + 1
@[simp]
theorem Fin.mk_bit0 {m : } {n : } (h : bit0 m < n) :
{ val := bit0 m, isLt := h } = bit0 { val := m, isLt := (_ : m < n) }
@[simp]
theorem Fin.mk_bit1 {m : } {n : } [inst : ] (h : bit1 m < n) :
{ val := bit1 m, isLt := h } = bit1 { val := m, isLt := (_ : m < n) }
@[simp]
theorem Fin.val_two {n : } :
2 = 2
@[simp]
theorem Fin.ofNat_eq_val (n : ) [inst : ] (a : ) :
= a
theorem Fin.val_cast_of_lt {n : } [inst : ] {a : } (h : a < n) :
a = a

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

theorem Fin.cast_val_eq_self {n : } [inst : ] (a : Fin n) :
a = a

Converting the value of a Fin (n + 1) to Fin (n + 1) results in the same value.

theorem Fin.cast_nat_eq_last (n : ) :
n =
theorem Fin.le_val_last {n : } (i : Fin (n + 1)) :
i n
theorem Fin.add_one_pos {n : } (i : Fin (n + 1)) (h : i < ) :
0 < i + 1
theorem Fin.one_pos {n : } :
0 < 1
theorem Fin.zero_ne_one {n : } :
0 1
@[simp]
theorem Fin.zero_eq_one_iff {n : } [inst : ] :
0 = 1 n = 1
@[simp]
theorem Fin.one_eq_zero_iff {n : } [inst : ] :
1 = 0 n = 1

### succ and casts into larger Fin types #

@[simp]
theorem Fin.val_succ {n : } (j : Fin n) :
↑() = j + 1
@[simp]
theorem Fin.succ_pos {n : } (a : Fin n) :
0 <
def Fin.succEmbedding (n : ) :
Fin n ↪o Fin (n + 1)

Fin.succ as an OrderEmbedding

Equations
@[simp]
theorem Fin.val_succEmbedding {n : } :
().toEmbedding = Fin.succ
@[simp]
theorem Fin.succ_le_succ_iff {n : } {a : Fin n} {b : Fin n} :
a b
@[simp]
theorem Fin.succ_lt_succ_iff {n : } {a : Fin n} {b : Fin n} :
a < b
@[simp]
theorem Fin.succ_inj {n : } {a : Fin n} {b : Fin n} :
a = b
theorem Fin.succ_ne_zero {n : } (k : Fin n) :
0
@[simp]
theorem Fin.succ_zero_eq_one {n : } [inst : ] :
= 1
@[simp]
theorem Fin.succ_zero_eq_one' {n : } :
= 1

Version of succ_zero_eq_one to be used by dsimp

@[simp]
theorem Fin.succ_one_eq_two {n : } [inst : ] :
= 2
@[simp]
theorem Fin.succ_one_eq_two' {n : } :
= 2

Version of succ_one_eq_two to be used by dsimp

@[simp]
theorem Fin.succ_mk (n : ) (i : ) (h : i < n) :
Fin.succ { val := i, isLt := h } = { val := i + 1, isLt := (_ : ) }
theorem Fin.mk_succ_pos {n : } (i : ) (h : i < n) :
0 < { val := , isLt := (_ : i + 1 < n + 1) }
theorem Fin.one_lt_succ_succ {n : } (a : Fin n) :
1 < Fin.succ ()
@[simp]
theorem Fin.add_one_lt_iff {n : } {k : Fin (n + 2)} :
k + 1 < k k = Fin.last (n + 1)
@[simp]
theorem Fin.add_one_le_iff {n : } {k : Fin (n + 1)} :
k + 1 k k =
@[simp]
theorem Fin.last_le_iff {n : } {k : Fin (n + 1)} :
k k =
@[simp]
theorem Fin.lt_add_one_iff {n : } {k : Fin (n + 1)} :
k < k + 1 k <
@[simp]
theorem Fin.le_zero_iff {n : } [inst : ] {k : Fin n} :
k 0 k = 0
theorem Fin.succ_succ_ne_one {n : } (a : Fin n) :
def Fin.castLt {n : } {m : } (i : Fin m) (h : i < n) :
Fin n

castLt i h embeds i into a Fin where h proves it belongs into.

Equations
• = { val := i, isLt := h }
@[simp]
theorem Fin.coe_castLt {n : } {m : } (i : Fin m) (h : i < n) :
↑() = i
@[simp]
theorem Fin.castLt_mk (i : ) (n : ) (m : ) (hn : i < n) (hm : i < m) :
Fin.castLt { val := i, isLt := hn } hm = { val := i, isLt := hm }
def Fin.castLe {n : } {m : } (h : n m) :

castLe h i embeds i into a larger Fin type.

Equations
@[simp]
theorem Fin.coe_castLe {n : } {m : } (h : n m) (i : Fin n) :
↑(().toEmbedding i) = i
@[simp]
theorem Fin.castLe_mk (i : ) (n : ) (m : ) (hn : i < n) (h : n m) :
().toEmbedding { val := i, isLt := hn } = { val := i, isLt := (_ : i < m) }
@[simp]
theorem Fin.castLe_zero {n : } {m : } (h : ) :
().toEmbedding 0 = 0
@[simp]
theorem Fin.range_castLe {n : } {k : } (h : n k) :
Set.range ().toEmbedding = { i | i < n }
@[simp]
theorem Fin.coe_of_injective_castLe_symm {n : } {k : } (h : n k) (i : Fin k) (hi : i Set.range ().toEmbedding) :
↑(↑(Equiv.symm (Equiv.ofInjective ().toEmbedding (_ : Function.Injective ().toEmbedding))) { val := i, property := hi }) = i
@[simp]
theorem Fin.castLe_succ {m : } {n : } (h : m + 1 n + 1) (i : Fin m) :
().toEmbedding () = Fin.succ ((Fin.castLe (_ : m n)).toEmbedding i)
@[simp]
theorem Fin.castLe_castLe {k : } {m : } {n : } (km : k m) (mn : m n) (i : Fin k) :
().toEmbedding (().toEmbedding i) = (Fin.castLe (_ : k n)).toEmbedding i
@[simp]
theorem Fin.castLe_comp_castLe {k : } {m : } {n : } (km : k m) (mn : m n) :
().toEmbedding ().toEmbedding = (Fin.castLe (_ : k n)).toEmbedding
def Fin.cast {n : } {m : } (eq : n = m) :

cast eq i embeds i into a equal Fin type, see also Equiv.finCongr.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Fin.symm_cast {n : } {m : } (h : n = m) :
= Fin.cast (_ : m = n)
theorem Fin.coe_cast {n : } {m : } (h : n = m) (i : Fin n) :
↑(().toEmbedding i) = i
@[simp]
theorem Fin.cast_zero {n : } {n' : } [inst : ] {h : n = n'} :
().toEmbedding 0 = 0
@[simp]
theorem Fin.cast_last {n : } {n' : } {h : n + 1 = n' + 1} :
().toEmbedding () = Fin.last n'
@[simp]
theorem Fin.cast_mk {n : } {m : } (h : n = m) (i : ) (hn : i < n) :
().toEmbedding { val := i, isLt := hn } = { val := i, isLt := (_ : i < m) }
@[simp]
theorem Fin.cast_trans {n : } {m : } {k : } (h : n = m) (h' : m = k) {i : Fin n} :
().toEmbedding (().toEmbedding i) = (RelIso.toRelEmbedding (Fin.cast (_ : n = k))).toEmbedding i
@[simp]
theorem Fin.cast_refl {n : } (h : optParam (n = n) (_ : n = n)) :
theorem Fin.castLe_of_eq {m : } {n : } (h : m = n) {h' : m n} :
().toEmbedding = ().toEmbedding
theorem Fin.cast_to_equiv {n : } {m : } (h : n = m) :
().toEquiv = Equiv.cast (_ : Fin n = Fin m)

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

theorem Fin.cast_eq_cast {n : } {m : } (h : n = m) :
().toEmbedding = (RelIso.toRelEmbedding (Fin.cast (_ : n = m))).toEmbedding

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

def Fin.castAdd {n : } (m : ) :
Fin n ↪o Fin (n + m)

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

Equations
@[simp]
theorem Fin.coe_castAdd {n : } (m : ) (i : Fin n) :
↑(().toEmbedding i) = i
@[simp]
theorem Fin.castAdd_zero {n : } :
().toEmbedding = (RelIso.toRelEmbedding (Fin.cast (_ : n = n))).toEmbedding
theorem Fin.castAdd_lt {m : } (n : ) (i : Fin m) :
↑(().toEmbedding i) < m
@[simp]
theorem Fin.castAdd_mk {n : } (m : ) (i : ) (h : i < n) :
().toEmbedding { val := i, isLt := h } = { val := i, isLt := (_ : i < n + m) }
@[simp]
theorem Fin.castAdd_castLt {n : } (m : ) (i : Fin (n + m)) (hi : i < n) :
().toEmbedding (Fin.castLt i hi) = i
@[simp]
theorem Fin.castLt_castAdd {n : } (m : ) (i : Fin n) :
Fin.castLt (().toEmbedding i) (_ : ↑(().toEmbedding i) < n) = i
theorem Fin.castAdd_cast {n : } {n' : } (m : ) (i : Fin n') (h : n' = n) :
().toEmbedding (().toEmbedding i) = (RelIso.toRelEmbedding (Fin.cast (_ : n' + m = n + m))).toEmbedding (().toEmbedding i)

For rewriting in the reverse direction, see Fin.cast_castAdd_left.

theorem Fin.cast_castAdd_left {n : } {n' : } {m : } (i : Fin n') (h : n' + m = n + m) :
().toEmbedding (().toEmbedding i) = ().toEmbedding ((RelIso.toRelEmbedding (Fin.cast (_ : n' = n))).toEmbedding i)
@[simp]
theorem Fin.cast_castAdd_right {n : } {m : } {m' : } (i : Fin n) (h : n + m' = n + m) :
().toEmbedding (().toEmbedding i) = ().toEmbedding i
theorem Fin.castAdd_castAdd {m : } {n : } {p : } (i : Fin m) :
().toEmbedding (().toEmbedding i) = (RelIso.toRelEmbedding (Fin.cast (_ : m + (n + p) = m + n + p))).toEmbedding ((Fin.castAdd (n + p)).toEmbedding i)
@[simp]
theorem Fin.cast_succ_eq {n : } {n' : } (i : Fin n) (h : = Nat.succ n') :
().toEmbedding () = Fin.succ ((RelIso.toRelEmbedding (Fin.cast (_ : n = n'))).toEmbedding i)

The cast of the successor is the succesor of the cast. See Fin.succ_cast_eq for rewriting in the reverse direction.

theorem Fin.succ_cast_eq {n : } {n' : } (i : Fin n) (h : n = n') :
Fin.succ (().toEmbedding i) = (RelIso.toRelEmbedding (Fin.cast (_ : = Nat.succ n'))).toEmbedding ()
def Fin.castSucc {n : } :
Fin n ↪o Fin (n + 1)

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

Equations
• Fin.castSucc =
@[simp]
theorem Fin.coe_castSucc {n : } (i : Fin n) :
↑(Fin.castSucc.toEmbedding i) = i
@[simp]
theorem Fin.castSucc_mk (n : ) (i : ) (h : i < n) :
Fin.castSucc.toEmbedding { val := i, isLt := h } = { val := i, isLt := (_ : i < ) }
@[simp]
theorem Fin.cast_castSucc {n : } {n' : } {h : n + 1 = n' + 1} {i : Fin n} :
().toEmbedding (Fin.castSucc.toEmbedding i) = Fin.castSucc.toEmbedding ((RelIso.toRelEmbedding (Fin.cast (_ : n = n'))).toEmbedding i)
theorem Fin.castSucc_lt_succ {n : } (i : Fin n) :
Fin.castSucc.toEmbedding i <
theorem Fin.le_castSucc_iff {n : } {i : Fin (n + 1)} {j : Fin n} :
i Fin.castSucc.toEmbedding j i <
theorem Fin.castSucc_lt_iff_succ_le {n : } {i : Fin n} {j : Fin (n + 1)} :
Fin.castSucc.toEmbedding i < j j
@[simp]
theorem Fin.succ_last (n : ) :
@[simp]
theorem Fin.succ_eq_last_succ {n : } (i : Fin ()) :
= Fin.last (n + 1) i =
@[simp]
theorem Fin.castSucc_cast_lt {n : } (i : Fin (n + 1)) (h : i < n) :
Fin.castSucc.toEmbedding () = i
@[simp]
theorem Fin.cast_lt_castSucc {n : } (a : Fin n) (h : a < n) :
Fin.castLt (Fin.castSucc.toEmbedding a) h = a
@[simp]
theorem Fin.castSucc_lt_castSucc_iff {n : } {a : Fin n} {b : Fin n} :
Fin.castSucc.toEmbedding a < Fin.castSucc.toEmbedding b a < b
theorem Fin.castSucc_injective (n : ) :
Function.Injective Fin.castSucc.toEmbedding
theorem Fin.castSucc_inj {n : } {a : Fin n} {b : Fin n} :
Fin.castSucc.toEmbedding a = Fin.castSucc.toEmbedding b a = b
theorem Fin.castSucc_lt_last {n : } (a : Fin n) :
Fin.castSucc.toEmbedding a <
@[simp]
theorem Fin.castSucc_zero {n : } [inst : ] :
Fin.castSucc.toEmbedding 0 = 0
@[simp]
theorem Fin.castSucc_one {n : } :
Fin.castSucc.toEmbedding 1 = 1
theorem Fin.castSucc_pos {n : } [inst : ] {i : Fin n} (h : 0 < i) :
0 < Fin.castSucc.toEmbedding i

castSucc i is positive when i is positive

@[simp]
theorem Fin.castSucc_eq_zero_iff {n : } [inst : ] (a : Fin n) :
Fin.castSucc.toEmbedding a = 0 a = 0
theorem Fin.castSucc_ne_zero_iff {n : } [inst : ] (a : Fin n) :
Fin.castSucc.toEmbedding a 0 a 0
theorem Fin.castSucc_fin_succ (n : ) (j : Fin n) :
Fin.castSucc.toEmbedding () = Fin.succ (Fin.castSucc.toEmbedding j)
@[simp]
theorem Fin.coe_eq_castSucc {n : } {a : Fin n} :
a = Fin.castSucc.toEmbedding a
@[simp]
theorem Fin.coeSucc_eq_succ {n : } {a : Fin n} :
Fin.castSucc.toEmbedding a + 1 =
theorem Fin.lt_succ {n : } {a : Fin n} :
Fin.castSucc.toEmbedding a <
@[simp]
theorem Fin.range_castSucc {n : } :
Set.range Fin.castSucc.toEmbedding = { i | i < n }
theorem Fin.exists_castSucc_eq {n : } {i : Fin (n + 1)} :
(j, Fin.castSucc.toEmbedding j = i) i
@[simp]
theorem Fin.coe_of_injective_castSucc_symm {n : } (i : Fin ()) (hi : i Set.range Fin.castSucc.toEmbedding) :
↑(↑(Equiv.symm (Equiv.ofInjective Fin.castSucc.toEmbedding (_ : Function.Injective Fin.castSucc.toEmbedding))) { val := i, property := hi }) = i
theorem Fin.succ_castSucc {n : } (i : Fin n) :
Fin.succ (Fin.castSucc.toEmbedding i) = Fin.castSucc.toEmbedding ()
def Fin.addNat {n : } (m : ) :
Fin n ↪o Fin (n + m)

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

Equations
@[simp]
theorem Fin.coe_addNat {n : } (m : ) (i : Fin n) :
↑(().toEmbedding i) = i + m
@[simp]
theorem Fin.addNat_one {n : } {i : Fin n} :
().toEmbedding i =
theorem Fin.le_coe_addNat {n : } (m : ) (i : Fin n) :
m ↑(().toEmbedding i)
@[simp]
theorem Fin.addNat_mk {m : } (n : ) (i : ) (hi : i < m) :
().toEmbedding { val := i, isLt := hi } = { val := i + n, isLt := (_ : i + n < m + n) }
@[simp]
theorem Fin.cast_addNat_zero {n : } {n' : } (i : Fin n) (h : n + 0 = n') :
().toEmbedding (().toEmbedding i) = (RelIso.toRelEmbedding (Fin.cast (_ : n = n'))).toEmbedding i
theorem Fin.addNat_cast {n : } {n' : } {m : } (i : Fin n') (h : n' = n) :
().toEmbedding (().toEmbedding i) = (RelIso.toRelEmbedding (Fin.cast (_ : n' + m = n + m))).toEmbedding (().toEmbedding i)

For rewriting in the reverse direction, see Fin.cast_addNat_left.

theorem Fin.cast_addNat_left {n : } {n' : } {m : } (i : Fin n') (h : n' + m = n + m) :
().toEmbedding (().toEmbedding i) = ().toEmbedding ((RelIso.toRelEmbedding (Fin.cast (_ : n' = n))).toEmbedding i)
@[simp]
theorem Fin.cast_addNat_right {n : } {m : } {m' : } (i : Fin n) (h : n + m' = n + m) :
().toEmbedding (().toEmbedding i) = ().toEmbedding i
def Fin.natAdd (n : ) {m : } :
Fin m ↪o Fin (n + m)

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

Equations
@[simp]
theorem Fin.coe_natAdd (n : ) {m : } (i : Fin m) :
↑(().toEmbedding i) = n + i
@[simp]
theorem Fin.natAdd_mk {m : } (n : ) (i : ) (hi : i < m) :
().toEmbedding { val := i, isLt := hi } = { val := n + i, isLt := (_ : n + i < n + m) }
theorem Fin.le_coe_natAdd {n : } (m : ) (i : Fin n) :
m ↑(().toEmbedding i)
theorem Fin.natAdd_cast {n : } {n' : } (m : ) (i : Fin n') (h : n' = n) :
().toEmbedding (().toEmbedding i) = (RelIso.toRelEmbedding (Fin.cast (_ : m + n' = m + n))).toEmbedding (().toEmbedding i)

For rewriting in the reverse direction, see Fin.cast_natAdd_right.

theorem Fin.cast_natAdd_right {n : } {n' : } {m : } (i : Fin n') (h : m + n' = m + n) :
().toEmbedding (().toEmbedding i) = ().toEmbedding ((RelIso.toRelEmbedding (Fin.cast (_ : n' = n))).toEmbedding i)
@[simp]
theorem Fin.cast_natAdd_left {n : } {m : } {m' : } (i : Fin n) (h : m' + n = m + n) :
().toEmbedding (().toEmbedding i) = ().toEmbedding i
theorem Fin.castAdd_natAdd (p : ) (m : ) {n : } (i : Fin n) :
().toEmbedding (().toEmbedding i) = (RelIso.toRelEmbedding (Fin.cast (_ : m + (n + p) = m + n + p))).toEmbedding (().toEmbedding (().toEmbedding i))
theorem Fin.natAdd_castAdd (p : ) (m : ) {n : } (i : Fin n) :
().toEmbedding (().toEmbedding i) = (RelIso.toRelEmbedding (Fin.cast (_ : m + n + p = m + (n + p)))).toEmbedding (().toEmbedding (().toEmbedding i))
theorem Fin.natAdd_natAdd (m : ) (n : ) {p : } (i : Fin p) :
().toEmbedding (().toEmbedding i) = (RelIso.toRelEmbedding (Fin.cast (_ : m + n + p = m + (n + p)))).toEmbedding ((Fin.natAdd (m + n)).toEmbedding i)
@[simp]
theorem Fin.cast_natAdd_zero {n : } {n' : } (i : Fin n) (h : 0 + n = n') :
().toEmbedding (().toEmbedding i) = (RelIso.toRelEmbedding (Fin.cast (_ : n = n'))).toEmbedding i
@[simp]
theorem Fin.cast_natAdd (n : ) {m : } (i : Fin m) :
(RelIso.toRelEmbedding (Fin.cast (_ : n + m = m + n))).toEmbedding (().toEmbedding i) = ().toEmbedding i
@[simp]
theorem Fin.cast_addNat {n : } (m : ) (i : Fin n) :
(RelIso.toRelEmbedding (Fin.cast (_ : n + m = m + n))).toEmbedding (().toEmbedding i) = ().toEmbedding i
@[simp]
theorem Fin.natAdd_last {m : } {n : } :
().toEmbedding () = Fin.last (n + m)
theorem Fin.natAdd_castSucc {m : } {n : } {i : Fin m} :
().toEmbedding (Fin.castSucc.toEmbedding i) = Fin.castSucc.toEmbedding (().toEmbedding i)

### pred #

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

Predecessor

Equations
• Fin.pred x x = match x, x with | { val := a, isLt := h₁ }, h₂ => { val := , isLt := (_ : < Nat.pred (n + 1)) }
@[simp]
theorem Fin.coe_pred {n : } (j : Fin (n + 1)) (h : j 0) :
↑(Fin.pred j h) = j - 1
@[simp]
theorem Fin.succ_pred {n : } (i : Fin (n + 1)) (h : i 0) :
@[simp]
theorem Fin.pred_succ {n : } (i : Fin n) {h : 0} :
Fin.pred () h = i
theorem Fin.pred_eq_iff_eq_succ {n : } (i : Fin (n + 1)) (hi : i 0) (j : Fin n) :
Fin.pred i hi = j i =
theorem Fin.pred_mk_succ {n : } (i : ) (h : i < n + 1) :
Fin.pred { val := i + 1, isLt := (_ : i + 1 < n + 1 + 1) } (_ : { val := i + 1, isLt := (_ : i + 1 < n + 1 + 1) } 0) = { val := i, isLt := h }
@[simp]
theorem Fin.pred_mk_succ' {n : } (i : ) (h₁ : i + 1 < n + 1 + 1) (h₂ : { val := i + 1, isLt := h₁ } 0) :
Fin.pred { val := i + 1, isLt := h₁ } h₂ = { val := i, isLt := (_ : i < n + 1) }
theorem Fin.pred_mk {n : } (i : ) (h : i < n + 1) (w : { val := i, isLt := h } 0) :
Fin.pred { val := i, isLt := h } w = { val := i - 1, isLt := (_ : i - 1 < n) }
@[simp]
theorem Fin.pred_le_pred_iff {n : } {a : Fin ()} {b : Fin ()} {ha : a 0} {hb : b 0} :
Fin.pred a ha Fin.pred b hb a b
@[simp]
theorem Fin.pred_lt_pred_iff {n : } {a : Fin ()} {b : Fin ()} {ha : a 0} {hb : b 0} :
Fin.pred a ha < Fin.pred b hb a < b
@[simp]
theorem Fin.pred_inj {n : } {a : Fin (n + 1)} {b : Fin (n + 1)} {ha : a 0} {hb : b 0} :
Fin.pred a ha = Fin.pred b hb a = b
@[simp]
theorem Fin.pred_one {n : } :
Fin.pred 1 (_ : 1 0) = 0
theorem Fin.pred_add_one {n : } (i : Fin (n + 2)) (h : i < n + 1) :
Fin.pred (i + 1) (_ : i + 1 0) =
def Fin.subNat {n : } (m : ) (i : Fin (n + m)) (h : m i) :
Fin n

subNat i h subtracts m from i, generalizes Fin.pred.

Equations
@[simp]
theorem Fin.coe_subNat {n : } {m : } (i : Fin (n + m)) (h : m i) :
↑(Fin.subNat m i h) = i - m
@[simp]
theorem Fin.subNat_mk {n : } {m : } {i : } (h₁ : i < n + m) (h₂ : m i) :
Fin.subNat m { val := i, isLt := h₁ } h₂ = { val := i - m, isLt := (_ : i - m < n) }
@[simp]
theorem Fin.pred_castSucc_succ {n : } (i : Fin n) :
Fin.pred (Fin.castSucc.toEmbedding ()) (_ : Fin.castSucc.toEmbedding () 0) = Fin.castSucc.toEmbedding i
@[simp]
theorem Fin.addNat_subNat {n : } {m : } {i : Fin (n + m)} (h : m i) :
().toEmbedding (Fin.subNat m i h) = i
@[simp]
theorem Fin.subNat_addNat {n : } (i : Fin n) (m : ) (h : optParam (m ↑(().toEmbedding i)) (_ : m ↑(().toEmbedding i))) :
Fin.subNat m (().toEmbedding i) h = i
@[simp]
theorem Fin.natAdd_subNat_cast {n : } {m : } {i : Fin (n + m)} (h : n i) :
().toEmbedding (Fin.subNat n ((RelIso.toRelEmbedding (Fin.cast (_ : n + m = m + n))).toEmbedding i) h) = i
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
• = { val := i / n, isLt := (_ : i / n < m) }
@[simp]
theorem Fin.coe_divNat {n : } {m : } (i : Fin (m * n)) :
↑() = 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
• = { val := i % n, isLt := (_ : i % n < n) }
@[simp]
theorem Fin.coe_modNat {n : } {m : } (i : Fin (m * n)) :
↑() = i % n

### recursion and induction principles #

def Fin.succRec {C : (n : ) → Fin nSort u_1} (H0 : (n : ) → C () 0) (Hs : (n : ) → (i : Fin n) → C n iC () ()) {n : } (i : Fin n) :
C n i

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.

Equations
def Fin.succRecOn {n : } (i : Fin n) {C : (n : ) → Fin nSort u_1} (H0 : (n : ) → C (n + 1) 0) (Hs : (n : ) → (i : Fin n) → C n iC () ()) :
C n i

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.

A version of Fin.succRec taking i : Fin n as the first argument.

Equations
@[simp]
theorem Fin.succRecOn_zero {C : (n : ) → Fin nSort u_1} {H0 : (n : ) → C (n + 1) 0} {Hs : (n : ) → (i : Fin n) → C n iC () ()} (n : ) :
Fin.succRecOn 0 H0 Hs = H0 n
@[simp]
theorem Fin.succRecOn_succ {C : (n : ) → Fin nSort u_1} {H0 : (n : ) → C (n + 1) 0} {Hs : (n : ) → (i : Fin n) → C n iC () ()} {n : } (i : Fin n) :
Fin.succRecOn () H0 Hs = Hs n i (Fin.succRecOn i H0 Hs)
def Fin.induction {n : } {C : Fin (n + 1)Sort u_1} (h0 : C 0) (hs : (i : Fin n) → C (Fin.castSucc.toEmbedding i)C ()) (i : Fin (n + 1)) :
C i

Define C i by induction on i : Fin (n + 1) via induction on the underlying Nat value. This function has two arguments: h0 handles the base case on C 0, and hs defines the inductive step using C i.castSucc.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Fin.induction_zero {n : } {C : Fin (n + 1)Sort u_1} (h0 : C 0) (hs : (i : Fin n) → C (Fin.castSucc.toEmbedding i)C ()) :
(fun i => Fin.induction h0 hs i) 0 = h0
@[simp]
theorem Fin.induction_succ {n : } {C : Fin (n + 1)Sort u_1} (h0 : C 0) (hs : (i : Fin n) → C (Fin.castSucc.toEmbedding i)C ()) (i : Fin n) :
(fun i => Fin.induction h0 hs i) () = hs i (Fin.induction h0 hs (Fin.castSucc.toEmbedding i))
def Fin.inductionOn {n : } (i : Fin (n + 1)) {C : Fin (n + 1)Sort u_1} (h0 : C 0) (hs : (i : Fin n) → C (Fin.castSucc.toEmbedding i)C ()) :
C i

Define C i by induction on i : Fin (n + 1) via induction on the underlying Nat value. This function has two arguments: h0 handles the base case on C 0, and hs defines the inductive step using C i.castSucc.

A version of Fin.induction taking i : Fin (n + 1) as the first argument.

Equations
def Fin.cases {n : } {C : Fin (n + 1)Sort u_1} (H0 : C 0) (Hs : (i : Fin n) → C ()) (i : Fin (n + 1)) :
C i

Define f : Π i : Fin n.succ, C i by separately handling the cases i = 0 and i = j.succ, j : Fin n.

Equations
@[simp]
theorem Fin.cases_zero {n : } {C : Fin (n + 1)Sort u_1} {H0 : C 0} {Hs : (i : Fin n) → C ()} :
Fin.cases H0 Hs 0 = H0
@[simp]
theorem Fin.cases_succ {n : } {C : Fin (n + 1)Sort u_1} {H0 : C 0} {Hs : (i : Fin n) → C ()} (i : Fin n) :
Fin.cases H0 Hs () = Hs i
@[simp]
theorem Fin.cases_succ' {n : } {C : Fin (n + 1)Sort u_1} {H0 : C 0} {Hs : (i : Fin n) → C ()} {i : } (h : i + 1 < n + 1) :
Fin.cases H0 Hs { val := , isLt := h } = Hs { val := i, isLt := (_ : i < n) }
theorem Fin.forall_fin_succ {n : } {P : Fin (n + 1)Prop} :
((i : Fin (n + 1)) → P i) P 0 ((i : Fin n) → P ())
theorem Fin.exists_fin_succ {n : } {P : Fin (n + 1)Prop} :
(i, P i) P 0 i, P ()
theorem Fin.forall_fin_one {p : Fin 1Prop} :
((i : Fin 1) → p i) p 0
theorem Fin.exists_fin_one {p : Fin 1Prop} :
(i, p i) p 0
theorem Fin.forall_fin_two {p : Fin 2Prop} :
((i : Fin 2) → p i) p 0 p 1
theorem Fin.exists_fin_two {p : Fin 2Prop} :
(i, p i) p 0 p 1
theorem Fin.fin_two_eq_of_eq_zero_iff {a : Fin 2} {b : Fin 2} (h : a = 0 b = 0) :
a = b
def Fin.reverseInduction {n : } {C : Fin (n + 1)Sort u_1} (hlast : C ()) (hs : (i : Fin n) → C ()C (Fin.castSucc.toEmbedding i)) (i : Fin (n + 1)) :
C i

Define C i by reverse induction on i : Fin (n + 1) via induction on the underlying Nat value. This function has two arguments: hlast handles the base case on C (Fin.last n), and hs defines the inductive step using C i.succ, inducting downwards.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Fin.reverse_induction_last {n : } {C : Fin (n + 1)Sort u_1} (h0 : C ()) (hs : (i : Fin n) → C ()C (Fin.castSucc.toEmbedding i)) :
@[simp]
theorem Fin.reverse_induction_castSucc {n : } {C : Fin (n + 1)Sort u_1} (h0 : C ()) (hs : (i : Fin n) → C ()C (Fin.castSucc.toEmbedding i)) (i : Fin n) :
Fin.reverseInduction h0 hs (Fin.castSucc.toEmbedding i) = hs i (Fin.reverseInduction h0 hs ())
def Fin.lastCases {n : } {C : Fin (n + 1)Sort u_1} (hlast : C ()) (hcast : (i : Fin n) → C (Fin.castSucc.toEmbedding i)) (i : Fin (n + 1)) :
C i

Define f : Π i : Fin n.succ, C i by separately handling the cases i = Fin.last n and i = j.castSucc, j : Fin n.

Equations
@[simp]
theorem Fin.lastCases_last {n : } {C : Fin (n + 1)Sort u_1} (hlast : C ()) (hcast : (i : Fin n) → C (Fin.castSucc.toEmbedding i)) :
Fin.lastCases hlast hcast () = hlast
@[simp]
theorem Fin.lastCases_castSucc {n : } {C : Fin (n + 1)Sort u_1} (hlast : C ()) (hcast : (i : Fin n) → C (Fin.castSucc.toEmbedding i)) (i : Fin n) :
Fin.lastCases hlast hcast (Fin.castSucc.toEmbedding i) = hcast i
def Fin.addCases {m : } {n : } {C : Fin (m + n)Sort u} (hleft : (i : Fin m) → C (().toEmbedding i)) (hright : (i : Fin n) → C (().toEmbedding i)) (i : Fin (m + n)) :
C i

Define f : Π i : Fin (m + n), C i by separately handling the cases i = castAdd n i, j : Fin m and i = natAdd m j, j : Fin n.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Fin.addCases_left {m : } {n : } {C : Fin (m + n)Sort u_1} (hleft : (i : Fin m) → C (().toEmbedding i)) (hright : (i : Fin n) → C (().toEmbedding i)) (i : Fin m) :
Fin.addCases hleft hright (().toEmbedding i) = hleft i
@[simp]
theorem Fin.addCases_right {m : } {n : } {C : Fin (m + n)Sort u_1} (hleft : (i : Fin m) → C (().toEmbedding i)) (hright : (i : Fin n) → C (().toEmbedding i)) (i : Fin n) :
Fin.addCases hleft hright (().toEmbedding i) = hright i
theorem Fin.lift_fun_iff_succ {n : } {α : Type u_1} (r : ααProp) [inst : IsTrans α r] {f : Fin (n + 1)α} :
((fun x x_1 => x < x_1) r) f f (i : Fin n) → r (f (Fin.castSucc.toEmbedding i)) (f ())
theorem Fin.strictMono_iff_lt_succ {n : } {α : Type u_1} [inst : ] {f : Fin (n + 1)α} :
∀ (i : Fin n), f (Fin.castSucc.toEmbedding i) < f ()

A function f on Fin (n + 1) is strictly monotone if and only if f i < f (i + 1) for all i.

theorem Fin.monotone_iff_le_succ {n : } {α : Type u_1} [inst : ] {f : Fin (n + 1)α} :
∀ (i : Fin n), f (Fin.castSucc.toEmbedding i) f ()

A function f on Fin (n + 1) is monotone if and only if f i ≤ f (i + 1) for all i.

theorem Fin.strictAnti_iff_succ_lt {n : } {α : Type u_1} [inst : ] {f : Fin (n + 1)α} :
∀ (i : Fin n), f () < f (Fin.castSucc.toEmbedding i)

A function f on Fin (n + 1) is strictly antitone if and only if f (i + 1) < f i for all i.

theorem Fin.antitone_iff_succ_le {n : } {α : Type u_1} [inst : ] {f : Fin (n + 1)α} :
∀ (i : Fin n), f () f (Fin.castSucc.toEmbedding i)

A function f on Fin (n + 1) is antitone if and only if f (i + 1) ≤ f i for all i.

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

Negation on Fin n

Equations
• = { neg := fun a => { val := (n - a) % n, isLt := (_ : (n - a) % n < n) } }
instance Fin.addCommGroup (n : ) [inst : ] :

Abelian group structure on Fin n.

Equations
theorem Fin.coe_neg {n : } (a : Fin n) :
↑(-a) = (n - a) % n
theorem Fin.coe_sub {n : } (a : Fin n) (b : Fin n) :
↑(a - b) = (a + (n - b)) % n
theorem Fin.fin_one_eq_zero (a : Fin 1) :
a = 0
@[simp]
theorem Fin.coe_fin_one (a : Fin 1) :
a = 0
@[simp]
theorem Fin.coe_neg_one {n : } :
↑(-1) = n
theorem Fin.coe_sub_one {n : } (a : Fin (n + 1)) :
↑(a - 1) = if a = 0 then n else a - 1
theorem Fin.coe_sub_iff_le {n : } {a : Fin n} {b : Fin n} :
↑(a - b) = a - b b a
theorem Fin.coe_sub_iff_lt {n : } {a : Fin n} {b : Fin n} :
↑(a - b) = n + a - b a < b
@[simp]
theorem Fin.lt_sub_one_iff {n : } {k : Fin (n + 2)} :
k < k - 1 k = 0
@[simp]
theorem Fin.le_sub_one_iff {n : } {k : Fin (n + 1)} :
k k - 1 k = 0
@[simp]
theorem Fin.sub_one_lt_iff {n : } {k : Fin (n + 1)} :
k - 1 < k 0 < k
theorem Fin.last_sub {n : } (i : Fin (n + 1)) :
- i = Fin.rev i
theorem Fin.succAbove_aux {n : } (p : Fin (n + 1)) :
StrictMono fun i => if Fin.castSucc.toEmbedding i < p then Fin.castSucc.toEmbedding i else
def Fin.succAbove {n : } (p : Fin (n + 1)) :
Fin n ↪o Fin (n + 1)

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

Equations
• One or more equations did not get rendered due to their size.
theorem Fin.succAbove_below {n : } (p : Fin (n + 1)) (i : Fin n) (h : Fin.castSucc.toEmbedding i < p) :
().toEmbedding i = Fin.castSucc.toEmbedding i

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.

@[simp]
theorem Fin.succAbove_ne_zero_zero {n : } [inst : ] {a : Fin (n + 1)} (ha : a 0) :
().toEmbedding 0 = 0
theorem Fin.succAbove_eq_zero_iff {n : } [inst : ] {a : Fin (n + 1)} {b : Fin n} (ha : a 0) :
().toEmbedding b = 0 b = 0
theorem Fin.succAbove_ne_zero {n : } [inst : ] {a : Fin (n + 1)} {b : Fin n} (ha : a 0) (hb : b 0) :
().toEmbedding b 0
@[simp]
theorem Fin.succAbove_zero {n : } :
().toEmbedding = Fin.succ

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

@[simp]
theorem Fin.succAbove_last {n : } :
= 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) :
().toEmbedding i = Fin.castSucc.toEmbedding i
theorem Fin.succAbove_above {n : } (p : Fin (n + 1)) (i : Fin n) (h : p Fin.castSucc.toEmbedding i) :
().toEmbedding i =

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_lt_ge {n : } (p : Fin (n + 1)) (i : Fin n) :
Fin.castSucc.toEmbedding i < p p Fin.castSucc.toEmbedding i

Embedding i : Fin n into Fin (n + 1) is always about some hole p.

theorem Fin.succAbove_lt_gt {n : } (p : Fin (n + 1)) (i : Fin n) :
Fin.castSucc.toEmbedding i < p p <

Embedding i : Fin n into Fin (n + 1) is always about some hole p.

@[simp]
theorem Fin.succAbove_lt_iff {n : } (p : Fin (n + 1)) (i : Fin n) :
().toEmbedding i < p Fin.castSucc.toEmbedding i < 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.lt_succAbove_iff {n : } (p : Fin (n + 1)) (i : Fin n) :
p < ().toEmbedding i p Fin.castSucc.toEmbedding i

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.succAbove_ne {n : } (p : Fin (n + 1)) (i : Fin n) :
().toEmbedding 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.succAbove_pos {n : } [inst : ] (p : Fin (n + 1)) (i : Fin n) (h : 0 < i) :
0 < ().toEmbedding i

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

@[simp]
theorem Fin.succAbove_castLt {n : } {x : Fin (n + 1)} {y : Fin (n + 1)} (h : x < y) (hx : optParam (x < n) (_ : x < n)) :
().toEmbedding (Fin.castLt x hx) = x
@[simp]
theorem Fin.succAbove_pred {n : } {x : Fin (n + 1)} {y : Fin (n + 1)} (h : x < y) (hy : optParam (y 0) (_ : y 0)) :
().toEmbedding (Fin.pred y hy) = y
theorem Fin.castLt_succAbove {n : } {x : Fin n} {y : Fin (n + 1)} (h : Fin.castSucc.toEmbedding x < y) (h' : optParam (↑(().toEmbedding x) < n) (_ : ↑(().toEmbedding x) < n)) :
Fin.castLt (().toEmbedding x) h' = x
theorem Fin.pred_succAbove {n : } {x : Fin n} {y : Fin (n + 1)} (h : y Fin.castSucc.toEmbedding x) (h' : optParam (().toEmbedding x 0) (_ : ().toEmbedding x 0)) :
Fin.pred (().toEmbedding x) h' = x
theorem Fin.exists_succAbove_eq {n : } {x : Fin (n + 1)} {y : Fin (n + 1)} (h : x y) :
z, ().toEmbedding z = x
@[simp]
theorem Fin.exists_succAbove_eq_iff {n : } {x : Fin (n + 1)} {y : Fin (n + 1)} :
(z, ().toEmbedding z = y) y x
@[simp]
theorem Fin.range_succAbove {n : } (p : Fin (n + 1)) :
Set.range ().toEmbedding = {p}

The range of p.succAbove is everything except p.

@[simp]
theorem Fin.range_succ (n : ) :
Set.range Fin.succ = {0}
@[simp]
theorem Fin.exists_succ_eq_iff {n : } {x : Fin (n + 1)} :
(y, = x) x 0
theorem Fin.succAbove_right_injective {n : } {x : Fin (n + 1)} :
Function.Injective ().toEmbedding

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

theorem Fin.succAbove_right_inj {n : } {a : Fin n} {b : Fin n} {x : Fin (n + 1)} :
().toEmbedding a = ().toEmbedding b a = b

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

succAbove is injective at the pivot

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

succAbove is injective at the pivot

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

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) :
().toEmbedding () = Fin.succ ()
@[simp]
theorem Fin.one_succAbove_one {n : } :
().toEmbedding 1 = 2
def Fin.predAbove {n : } (p : Fin n) (i : Fin (n + 1)) :
Fin n

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

Equations
theorem Fin.predAbove_left_monotone {n : } (i : Fin (n + 1)) :
Monotone fun p =>
def Fin.castPred {n : } (i : Fin (n + 2)) :
Fin (n + 1)

castPred embeds i : Fin (n + 2) into Fin (n + 1) by lowering just last (n + 1) to last n.

Equations
@[simp]
theorem Fin.castPred_zero {n : } :
@[simp]
theorem Fin.castPred_one {n : } :
@[simp]
theorem Fin.predAbove_zero {n : } {i : Fin (n + 2)} (hi : i 0) :
= Fin.pred i hi
@[simp]
theorem Fin.castPred_last {n : } :
theorem Fin.castPred_mk (n : ) (i : ) (h : i < n + 1) :
Fin.castPred { val := i, isLt := (_ : i < Nat.succ (n + 1)) } = { val := i, isLt := h }
@[simp]
theorem Fin.castPred_mk' (n : ) (i : ) (h₁ : i < n + 2) (h₂ : i < n + 1) :
Fin.castPred { val := i, isLt := h₁ } = { val := i, isLt := h₂ }
theorem Fin.coe_castPred {n : } (a : Fin (n + 2)) (hx : a < Fin.last (n + 1)) :
↑() = a
theorem Fin.predAbove_below {n : } (p : Fin (n + 1)) (i : Fin (n + 2)) (h : i Fin.castSucc.toEmbedding p) :
@[simp]
theorem Fin.predAbove_last {n : } :
= Fin.castPred
theorem Fin.predAbove_last_apply {n : } (i : Fin n) :
Fin.predAbove () i = Fin.castPred i
theorem Fin.predAbove_above {n : } (p : Fin n) (i : Fin (n + 1)) (h : Fin.castSucc.toEmbedding p < i) :
= Fin.pred i (_ : i 0)
theorem Fin.castPred_monotone {n : } :
Monotone Fin.castPred
@[simp]
theorem Fin.succAbove_predAbove {n : } {p : Fin n} {i : Fin (n + 1)} (h : i Fin.castSucc.toEmbedding p) :
(Fin.succAbove (Fin.castSucc.toEmbedding p)).toEmbedding () = 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) :
Fin.predAbove p ((Fin.succAbove (Fin.castSucc.toEmbedding p)).toEmbedding 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.

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

pred commutes with succAbove.

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

succ commutes with predAbove.

@[simp]
theorem Fin.castPred_castSucc {n : } (i : Fin (n + 1)) :
Fin.castPred (Fin.castSucc.toEmbedding i) = i
theorem Fin.castSucc_castPred {n : } {i : Fin (n + 2)} (h : i < Fin.last (n + 1)) :
Fin.castSucc.toEmbedding () = i
theorem Fin.coe_castPred_le_self {n : } (i : Fin (n + 2)) :
↑() i
theorem Fin.coe_castPred_lt_iff {n : } {i : Fin (n + 2)} :
↑() < i i = Fin.last (n + 1)
theorem Fin.lt_last_iff_coe_castPred {n : } {i : Fin (n + 2)} :
i < Fin.last (n + 1) ↑() = i
def Fin.clamp (n : ) (m : ) :
Fin (m + 1)

min n m as an element of Fin (m + 1)

Equations
@[simp]
theorem Fin.coe_clamp (n : ) (m : ) :
↑() = min n m
@[simp]
theorem Fin.coe_ofNat_eq_mod (m : ) (n : ) [inst : ] :
n = n % m

### mul #

theorem Fin.val_mul {n : } (a : Fin n) (b : Fin n) :
↑(a * b) = a * b % n
theorem Fin.coe_mul {n : } (a : Fin n) (b : Fin n) :
↑(a * b) = a * b % n
theorem Fin.mul_one {n : } [inst : ] (k : Fin n) :
k * 1 = k
theorem Fin.mul_comm {n : } (a : Fin n) (b : Fin n) :
a * b = b * a
theorem Fin.one_mul {n : } [inst : ] (k : Fin n) :
1 * k = k
theorem Fin.mul_zero {n : } [inst : ] (k : Fin n) :
k * 0 = 0
theorem Fin.zero_mul {n : } [inst : ] (k : Fin n) :
0 * k = 0