data.fin.basic

# The finite type with `n` elements #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

• `fin_zero_elim` : Elimination principle for the empty set `fin 0`, generalizes `fin.elim0`.
• `fin.succ_rec` : 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.succ_rec_on` : same as `fin.succ_rec` 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.induction_on` : 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.reverse_induction`: reverse induction on `i : fin (n + 1)`; given `C (fin.last n)` and `∀ i : fin n, C (fin.succ i) → C (fin.cast_succ i)`, constructs all values `C i` by going down;
• `fin.last_cases`: define `f : Π i, fin (n + 1), C i` by separately handling the cases `i = fin.last n` and `i = fin.cast_succ j`, a special case of `fin.reverse_induction`;
• `fin.add_cases`: define a function on `fin (m + n)` by separately handling the cases `fin.cast_add n i` and `fin.nat_add m i`;
• `fin.succ_above_cases`: given `i : fin (n + 1)`, define a function on `fin (n + 1)` by separately handling the cases `j = i` and `j = fin.succ_above i k`, same as `fin.insert_nth` but marked as eliminator and works for `Sort*`.

### Order embeddings and an order isomorphism #

• `fin.order_iso_subtype` : coercion to `{ i // i < n }` as an `order_iso`;
• `fin.coe_embedding` : coercion to natural numbers as an `embedding`;
• `fin.coe_order_embedding` : coercion to natural numbers as an `order_embedding`;
• `fin.succ_embedding` : `fin.succ` as an `order_embedding`;
• `fin.cast_le h` : embed `fin n` into `fin m`, `h : n ≤ m`;
• `fin.cast eq` : order isomorphism between `fin n` and fin m`provided that`n = m`, see also`equiv.fin_congr`;
• `fin.cast_add m` : embed `fin n` into `fin (n+m)`;
• `fin.cast_succ` : embed `fin n` into `fin (n+1)`;
• `fin.succ_above p` : embed `fin n` into `fin (n + 1)` with a hole around `p`;
• `fin.add_nat m i` : add `m` on `i` on the right, generalizes `fin.succ`;
• `fin.nat_add n i` adds `n` on `i` on the left;

### Other casts #

• `fin.of_nat'`: given a positive number `n` (deduced from `[ne_zero n]`), `fin.of_nat' i` is `i % n` interpreted as an element of `fin n`;
• `fin.cast_lt i h` : embed `i` into a `fin` where `h` proves it belongs into;
• `fin.pred_above (p : fin n) i` : embed `i : fin (n+1)` into `fin n` by subtracting one if `p < i`;
• `fin.cast_pred` : embed `fin (n + 2)` into `fin (n + 1)` by mapping `fin.last (n + 1)` to `fin.last n`;
• `fin.sub_nat 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.div_nat i` : divides `i : fin (m * n)` by `n`;
• `fin.mod_nat 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 fin_zero_elim {α : fin 0 Sort u} (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
@[protected, instance]
def fin.fin_to_nat (n : ) :
Equations
theorem fin.val_injective {n : } :
@[protected]
theorem fin.prop {n : } (a : fin n) :
a.val < n
@[simp]
theorem fin.is_lt {n : } (a : fin n) :
a < n
@[protected]
theorem fin.pos {n : } (i : fin n) :
0 < n
theorem fin.pos_iff_nonempty {n : } :
0 < n nonempty (fin n)
def fin.equiv_subtype {n : } :
fin n {i // i < n}

Equivalence between `fin n` and `{ i // i < n }`.

Equations
@[simp]
theorem fin.equiv_subtype_symm_apply {n : } (a : {i // i < n}) :
= a.val, _⟩
@[simp]
theorem fin.equiv_subtype_apply {n : } (a : fin n) :
= a.val, _⟩

### coercions and constructions #

@[protected, simp]
theorem fin.eta {n : } (a : fin n) (h : a < n) :
a, h⟩ = a
@[ext]
theorem fin.ext {n : } {a b : fin n} (h : a = b) :
a = b
theorem fin.ext_iff {n : } {a b : fin n} :
a = b a = b
theorem fin.coe_injective {n : } :
theorem fin.coe_eq_coe {n : } (a b : fin n) :
a = b a = b
theorem fin.eq_iff_veq {n : } (a b : fin n) :
a = b a.val = b.val
theorem fin.ne_iff_vne {n : } (a b : fin n) :
a b a.val b.val
@[simp, nolint]
theorem fin.mk_eq_mk {n a : } {h : a < n} {a' : } {h' : a' < n} :
a, h⟩ = a', h'⟩ a = a'
@[protected]
theorem fin.mk.inj_iff {n a b : } {ha : a < n} {hb : b < n} :
a, ha⟩ = b, hb⟩ a = b
theorem fin.mk_val {m n : } (h : m < n) :
m, h⟩.val = m
theorem fin.eq_mk_iff_coe_eq {n : } {a : fin n} {k : } {hk : k < n} :
a = k, hk⟩ a = k
@[simp, norm_cast]
theorem fin.coe_mk {m n : } (h : m < n) :
m, h⟩ = m
theorem fin.mk_coe {n : } (i : fin n) :
i, _⟩ = i
theorem fin.coe_eq_val {n : } (a : fin n) :
a = a.val
@[simp]
theorem fin.val_eq_coe {n : } (a : fin n) :
a.val = a
@[protected]
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).

@[protected]
theorem fin.heq_ext_iff {k l : } (h : k = l) {i : fin k} {j : fin l} :
i == j i = j
theorem fin.exists_iff {n : } {p : fin n Prop} :
( (i : fin n), p i) (i : ) (h : i < n), p i, h⟩
theorem fin.forall_iff {n : } {p : fin n Prop} :
( (i : fin n), p i) (i : ) (h : i < n), p i, 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_coe_lt_coe {n : } {a b : fin n} :
a < b a < b
theorem fin.le_iff_coe_le_coe {n : } {a b : fin n} :
a b a b
theorem fin.mk_lt_of_lt_coe {n : } {b : fin n} {a : } (h : a < b) :
a, _⟩ < b
theorem fin.mk_le_of_le_coe {n : } {b : fin n} {a : } (h : a b) :
a, _⟩ b
@[simp, norm_cast]
theorem fin.coe_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, norm_cast]
theorem fin.coe_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`.

@[protected, instance]
Equations
@[simp]
theorem fin.mk_le_mk {n x y : } {hx : x < n} {hy : y < n} :
x, hx⟩ y, hy⟩ x y
@[simp]
theorem fin.mk_lt_mk {n x y : } {hx : x < n} {hy : y < n} :
x, hx⟩ < y, hy⟩ x < y
@[simp]
theorem fin.min_coe {n : } {a : fin n} :
= a
@[simp]
theorem fin.max_coe {n : } {a : fin n} :
= n
@[protected, instance]
Equations
theorem fin.coe_strict_mono {n : } :
def fin.order_iso_subtype {n : } :
fin n ≃o {i // i < n}

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

Equations
@[simp]
theorem fin.order_iso_subtype_apply {n : } (a : fin n) :
= a, _⟩
@[simp]
theorem fin.order_iso_subtype_symm_apply {n : } (a : {i // i < n}) :
= a, _⟩
def fin.coe_embedding {n : } :

The inclusion map `fin n → ℕ` is an embedding.

Equations
@[simp]
theorem fin.coe_embedding_apply {n : } (ᾰ : fin n) :
@[simp]
theorem fin.coe_order_embedding_apply (n : ) (ᾰ : fin n) :
=

The inclusion map `fin n → ℕ` is an order embedding.

Equations
@[protected, instance]

The ordering on `fin n` is a well order.

@[protected, instance]
def fin.has_well_founded {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 `has_well_founded` instance:

``````def factorial {n : ℕ} : fin n → ℕ
| ⟨0, _⟩ := 1
| ⟨i + 1, hi⟩ := (i + 1) * factorial ⟨i, i.lt_succ_self.trans hi⟩
``````
Equations
@[protected, instance]
Equations
def fin.of_nat' {n : } [ne_zero n] (i : ) :
fin n

Given a positive `n`, `fin.of_nat' i` is `i % n` as an element of `fin n`.

Equations
@[protected, instance]
Equations
@[simp]
theorem fin.coe_zero (n : ) [ne_zero n] :
0 = 0
@[simp]
theorem fin.val_zero' (n : ) [ne_zero n] :
0.val = 0
@[simp]
theorem fin.mk_zero {n : } [ne_zero n] :
0, _⟩ = 0
@[simp]
theorem fin.zero_le {n : } [ne_zero n] (a : fin n) :
0 a
theorem fin.zero_lt_one {n : } :
0 < 1
@[simp]
theorem fin.not_lt_zero {n : } (a : fin n.succ) :
¬a < 0
theorem fin.pos_iff_ne_zero {n : } [ne_zero n] (a : fin n) :
0 < a a 0
theorem fin.eq_zero_or_eq_succ {n : } (i : fin (n + 1)) :
i = 0 (j : fin n), i = j.succ
theorem fin.eq_succ_of_ne_zero {n : } {i : fin (n + 1)} (hi : i 0) :
(j : fin n), i = j.succ
def fin.rev {n : } :

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

Equations
@[simp]
theorem fin.coe_rev {n : } (i : fin n) :
(fin.rev i) = n - (i + 1)
theorem fin.rev_involutive {n : } :
theorem fin.rev_injective {n : } :
theorem fin.rev_surjective {n : } :
theorem fin.rev_bijective {n : } :
@[simp]
theorem fin.rev_inj {n : } {i j : fin n} :
i = j
@[simp]
theorem fin.rev_rev {n : } (i : fin n) :
@[simp]
theorem fin.rev_symm {n : } :
theorem fin.rev_eq {n a : } (i : fin (n + 1)) (h : n = a + i) :
= a, _⟩
@[simp]
theorem fin.rev_le_rev {n : } {i j : fin n} :
j i
@[simp]
theorem fin.rev_lt_rev {n : } {i j : fin n} :
j < i
@[simp]
theorem fin.rev_order_iso_apply {n : } (ᾰ : (fin n)ᵒᵈ) :
def fin.rev_order_iso {n : } :

`fin.rev n` as an order-reversing isomorphism.

Equations
@[simp]
@[simp]
theorem fin.rev_order_iso_symm_apply {n : } (i : fin n) :
def fin.last (n : ) :
fin (n + 1)

The greatest value of `fin (n+1)`

Equations
@[simp, norm_cast]
theorem fin.coe_last (n : ) :
theorem fin.last_val (n : ) :
(fin.last n).val = n
theorem fin.le_last {n : } (i : fin (n + 1)) :
i
@[protected, instance]
def fin.bounded_order {n : } :
Equations
@[protected, instance]
def fin.lattice {n : } :
lattice (fin (n + 1))
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.top_eq_last (n : ) :
theorem fin.bot_eq_zero (n : ) :
= 0
@[simp]
theorem fin.coe_order_iso_apply {n m : } (e : fin n ≃o fin m) (i : fin n) :
(e i) = i

If `e` is an `order_iso` 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 : ℕ)`.

@[protected, instance]
def fin.order_iso_subsingleton {n : } {α : Type u_1} [preorder α] :
@[protected, instance]
def fin.order_iso_subsingleton' {n : } {α : Type u_1} [preorder α] :
@[protected, instance]
def fin.order_iso_unique {n : } :
Equations
theorem fin.strict_mono_unique {n : } {α : Type u_1} [preorder α] {f g : fin n α} (hf : strict_mono f) (hg : strict_mono g) (h : = ) :
f = g

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

theorem fin.order_embedding_eq {n : } {α : Type u_1} [preorder α] {f g : fin n ↪o α} (h : = ) :
f = g

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

### addition, numerals, and coercion from nat #

theorem fin.one_val {n : } :
1.val = 1 % (n + 1)
theorem fin.coe_one' (n : ) [ne_zero n] :
1 = 1 % n
@[simp]
theorem fin.val_one (n : ) :
1.val = 1
@[simp]
theorem fin.coe_one (n : ) :
1 = 1
@[simp]
theorem fin.mk_one {n : } :
1, _⟩ = 1
@[protected, instance]
def fin.nontrivial {n : } :
nontrivial (fin (n + 2))
@[protected, instance]
Equations
@[protected, simp]
theorem fin.add_zero {n : } [ne_zero n] (k : fin n) :
k + 0 = k
@[protected, simp]
theorem fin.zero_add {n : } [ne_zero n] (k : fin n) :
0 + k = k
@[protected, instance]
def fin.add_comm_monoid (n : ) [ne_zero n] :
Equations
@[protected, instance]
Equations
theorem fin.val_add {n : } (a b : fin n) :
(a + b).val = (a.val + b.val) % n
theorem fin.coe_add {n : } (a b : fin n) :
(a + b) = (a + b) % n
theorem fin.coe_add_eq_ite {n : } (a b : fin n) :
(a + b) = ite (n a + b) (a + b - n) (a + b)
theorem fin.coe_bit0 {n : } (k : fin n) :
(bit0 k) = % n
theorem fin.coe_bit1 {n : } [ne_zero n] (k : fin n) :
(bit1 k) = % n
theorem fin.coe_add_one_of_lt {n : } {i : fin n.succ} (h : i < ) :
(i + 1) = i + 1
@[simp]
theorem fin.last_add_one (n : ) :
+ 1 = 0
theorem fin.coe_add_one {n : } (i : fin (n + 1)) :
(i + 1) = ite (i = fin.last n) 0 (i + 1)
@[simp]
theorem fin.mk_bit0 {m n : } (h : bit0 m < n) :
bit0 m, h⟩ = bit0 m, _⟩
@[simp]
theorem fin.mk_bit1 {m n : } [ne_zero n] (h : bit1 m < n) :
bit1 m, h⟩ = bit1 m, _⟩
@[simp]
theorem fin.val_two {n : } :
2.val = 2
@[simp]
theorem fin.coe_two {n : } :
2 = 2
@[simp]
theorem fin.of_nat_eq_coe (n a : ) :
= a
@[simp]
theorem fin.of_nat'_eq_coe (n : ) [ne_zero n] (a : ) :
theorem fin.coe_val_of_lt {n : } [ne_zero n] {a : } (h : a < n) :
a.val = a

Converting an in-range number to `fin n` produces a result whose value is the original number.

theorem fin.coe_val_eq_self {n : } [ne_zero n] (a : fin n) :
(a.val) = a

Converting the value of a `fin n` to `fin n` results in the same value.

theorem fin.coe_coe_of_lt {n : } [ne_zero n] {a : } (h : a < n) :

Coercing an in-range number to `fin n`, and converting back to `ℕ`, results in that number.

@[simp]
theorem fin.coe_coe_eq_self {n : } [ne_zero n] (a : fin n) :

Converting a `fin n` to `ℕ` and back results in the same value.

theorem fin.coe_nat_eq_last (n : ) :
n =
theorem fin.le_coe_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 : } [ne_zero n] :
0 = 1 n = 1
@[simp]
theorem fin.one_eq_zero_iff {n : } [ne_zero n] :
1 = 0 n = 1

### succ and casts into larger fin types #

@[simp]
theorem fin.coe_succ {n : } (j : fin n) :
(j.succ) = j + 1
@[simp]
theorem fin.succ_pos {n : } (a : fin n) :
0 < a.succ
def fin.succ_embedding (n : ) :
fin n ↪o fin (n + 1)

`fin.succ` as an `order_embedding`

Equations
@[simp]
theorem fin.coe_succ_embedding {n : } :
@[simp]
theorem fin.succ_le_succ_iff {n : } {a b : fin n} :
a.succ b.succ a b
@[simp]
theorem fin.succ_lt_succ_iff {n : } {a b : fin n} :
a.succ < b.succ a < b
theorem fin.succ_injective (n : ) :
@[simp]
theorem fin.succ_inj {n : } {a b : fin n} :
a.succ = b.succ a = b
theorem fin.succ_ne_zero {n : } (k : fin n) :
k.succ 0
@[simp]
theorem fin.succ_zero_eq_one {n : } [ne_zero n] :
0.succ = 1
@[simp]
theorem fin.succ_zero_eq_one' {n : } :
0.succ = 1

Version of `succ_zero_eq_one` to be used by `dsimp`

@[simp]
theorem fin.succ_one_eq_two {n : } [ne_zero n] :
1.succ = 2
@[simp]
theorem fin.succ_one_eq_two' {n : } :
1.succ = 2

Version of `succ_one_eq_two` to be used by `dsimp`

@[simp]
theorem fin.succ_mk (n i : ) (h : i < n) :
i, h⟩.succ = i + 1, _⟩
theorem fin.mk_succ_pos {n : } (i : ) (h : i < n) :
0 < i.succ, _⟩
theorem fin.one_lt_succ_succ {n : } (a : fin n) :
1 < a.succ.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 : } [ne_zero n] {k : fin n} :
k 0 k = 0
theorem fin.succ_succ_ne_one {n : } (a : fin n) :
def fin.cast_lt {n m : } (i : fin m) (h : i.val < n) :
fin n

`cast_lt i h` embeds `i` into a `fin` where `h` proves it belongs into.

Equations
@[simp]
theorem fin.coe_cast_lt {n m : } (i : fin m) (h : i.val < n) :
@[simp]
theorem fin.cast_lt_mk (i n m : ) (hn : i < n) (hm : i < m) :
i, hn⟩.cast_lt hm = i, hm⟩
def fin.cast_le {n m : } (h : n m) :

`cast_le h i` embeds `i` into a larger `fin` type.

Equations
@[simp]
theorem fin.coe_cast_le {n m : } (h : n m) (i : fin n) :
@[simp]
theorem fin.cast_le_mk (i n m : ) (hn : i < n) (h : n m) :
(fin.cast_le h) i, hn⟩ = i, _⟩
@[simp]
theorem fin.cast_le_zero {n m : } (h : n.succ m.succ) :
@[simp]
theorem fin.range_cast_le {n k : } (h : n k) :
= {i : fin k | i < n}
@[simp]
theorem fin.coe_of_injective_cast_le_symm {n k : } (h : n k) (i : fin k) (hi : i ) :
( _).symm) i, hi⟩) = i
@[simp]
theorem fin.cast_le_succ {m n : } (h : m + 1 n + 1) (i : fin m) :
@[simp]
theorem fin.cast_le_cast_le {k m n : } (km : k m) (mn : m n) (i : fin k) :
@[simp]
theorem fin.cast_le_comp_cast_le {k m n : } (km : k m) (mn : m n) :
def fin.cast {n m : } (eq : n = m) :

`cast eq i` embeds `i` into a equal `fin` type, see also `equiv.fin_congr`.

Equations
@[simp]
theorem fin.symm_cast {n m : } (h : n = m) :
@[simp]
theorem fin.coe_cast {n m : } (h : n = m) (i : fin n) :

While `fin.coe_order_iso_apply` is a more general case of this, we mark this `simp` anyway as it is eligible for `dsimp`.

@[simp]
theorem fin.cast_zero {n n' : } [ne_zero n] {h : n = n'} :
(fin.cast h) 0 = 0
@[simp]
theorem fin.cast_last {n n' : } {h : n + 1 = n' + 1} :
@[simp]
theorem fin.cast_mk {n m : } (h : n = m) (i : ) (hn : i < n) :
(fin.cast h) i, hn⟩ = i, _⟩
@[simp]
theorem fin.cast_trans {n m k : } (h : n = m) (h' : m = k) {i : fin n} :
@[simp]
theorem fin.cast_refl {n : } (h : n = n := rfl) :
=
theorem fin.cast_le_of_eq {m n : } (h : m = n) {h' : m n} :
theorem fin.cast_to_equiv {n m : } (h : n = 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) :

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

def fin.cast_add {n : } (m : ) :
fin n ↪o fin (n + m)

`cast_add m i` embeds `i : fin n` in `fin (n+m)`. See also `fin.nat_add` and `fin.add_nat`.

Equations
@[simp]
theorem fin.coe_cast_add {n : } (m : ) (i : fin n) :
@[simp]
theorem fin.cast_add_zero {n : } :
theorem fin.cast_add_lt {m : } (n : ) (i : fin m) :
@[simp]
theorem fin.cast_add_mk {n : } (m i : ) (h : i < n) :
(fin.cast_add m) i, h⟩ = i, _⟩
@[simp]
theorem fin.cast_add_cast_lt {n : } (m : ) (i : fin (n + m)) (hi : i.val < n) :
@[simp]
theorem fin.cast_lt_cast_add {n : } (m : ) (i : fin n) :
theorem fin.cast_add_cast {n n' : } (m : ) (i : fin n') (h : n' = n) :

For rewriting in the reverse direction, see `fin.cast_cast_add_left`.

theorem fin.cast_cast_add_left {n n' m : } (i : fin n') (h : n' + m = n + m) :
@[simp]
theorem fin.cast_cast_add_right {n m m' : } (i : fin n) (h : n + m' = n + m) :
theorem fin.cast_add_cast_add {m n p : } (i : fin m) :
@[simp]
theorem fin.cast_succ_eq {n n' : } (i : fin n) (h : n.succ = n'.succ) :

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') :
def fin.cast_succ {n : } :
fin n ↪o fin (n + 1)

`cast_succ i` embeds `i : fin n` in `fin (n+1)`.

Equations
@[simp]
theorem fin.coe_cast_succ {n : } (i : fin n) :
@[simp]
theorem fin.cast_succ_mk (n i : ) (h : i < n) :
fin.cast_succ i, h⟩ = i, _⟩
@[simp]
theorem fin.cast_cast_succ {n n' : } {h : n + 1 = n' + 1} {i : fin n} :
theorem fin.cast_succ_lt_succ {n : } (i : fin n) :
theorem fin.le_cast_succ_iff {n : } {i : fin (n + 1)} {j : fin n} :
i < j.succ
theorem fin.cast_succ_lt_iff_succ_le {n : } {i : fin n} {j : fin (n + 1)} :
i.succ j
@[simp]
theorem fin.succ_last (n : ) :
@[simp]
theorem fin.succ_eq_last_succ {n : } (i : fin n.succ) :
i.succ = fin.last (n + 1) i =
@[simp]
theorem fin.cast_succ_cast_lt {n : } (i : fin (n + 1)) (h : i < n) :
@[simp]
theorem fin.cast_lt_cast_succ {n : } (a : fin n) (h : a < n) :
h = a
@[simp]
theorem fin.cast_succ_lt_cast_succ_iff {n : } {a b : fin n} :
a < b
theorem fin.cast_succ_inj {n : } {a b : fin n} :
a = b
theorem fin.cast_succ_lt_last {n : } (a : fin n) :
@[simp]
theorem fin.cast_succ_zero {n : } [ne_zero n] :
@[simp]
theorem fin.cast_succ_one {n : } :
theorem fin.cast_succ_pos {n : } [ne_zero n] {i : fin n} (h : 0 < i) :

`cast_succ i` is positive when `i` is positive

@[simp]
theorem fin.cast_succ_eq_zero_iff {n : } [ne_zero n] (a : fin n) :
a = 0
theorem fin.cast_succ_ne_zero_iff {n : } [ne_zero n] (a : fin n) :
a 0
theorem fin.cast_succ_fin_succ (n : ) (j : fin n) :
@[simp, norm_cast]
theorem fin.coe_eq_cast_succ {n : } {a : fin n} :
@[simp]
theorem fin.coe_succ_eq_succ {n : } {a : fin n} :
= a.succ
theorem fin.lt_succ {n : } {a : fin n} :
@[simp]
theorem fin.range_cast_succ {n : } :
= {i : fin (n + 1) | i < n}
@[simp]
theorem fin.coe_of_injective_cast_succ_symm {n : } (i : fin (n + 1)) (hi : i ) :
i, hi⟩) = i
theorem fin.succ_cast_succ {n : } (i : fin n) :
def fin.add_nat {n : } (m : ) :
fin n ↪o fin (n + m)

`add_nat m i` adds `m` to `i`, generalizes `fin.succ`.

Equations
@[simp]
theorem fin.coe_add_nat {n : } (m : ) (i : fin n) :
@[simp]
theorem fin.add_nat_one {n : } {i : fin n} :
theorem fin.le_coe_add_nat {n : } (m : ) (i : fin n) :
@[simp]
theorem fin.add_nat_mk {m : } (n i : ) (hi : i < m) :
(fin.add_nat n) i, hi⟩ = i + n, _⟩
@[simp]
theorem fin.cast_add_nat_zero {n n' : } (i : fin n) (h : n + 0 = n') :
theorem fin.add_nat_cast {n n' m : } (i : fin n') (h : n' = n) :

For rewriting in the reverse direction, see `fin.cast_add_nat_left`.

theorem fin.cast_add_nat_left {n n' m : } (i : fin n') (h : n' + m = n + m) :
@[simp]
theorem fin.cast_add_nat_right {n m m' : } (i : fin n) (h : n + m' = n + m) :
def fin.nat_add (n : ) {m : } :
fin m ↪o fin (n + m)

`nat_add n i` adds `n` to `i` "on the left".

Equations
@[simp]
theorem fin.coe_nat_add (n : ) {m : } (i : fin m) :
@[simp]
theorem fin.nat_add_mk {m : } (n i : ) (hi : i < m) :
(fin.nat_add n) i, hi⟩ = n + i, _⟩
theorem fin.le_coe_nat_add {n : } (m : ) (i : fin n) :
theorem fin.nat_add_zero {n : } :
theorem fin.nat_add_cast {n n' : } (m : ) (i : fin n') (h : n' = n) :

For rewriting in the reverse direction, see `fin.cast_nat_add_right`.

theorem fin.cast_nat_add_right {n n' m : } (i : fin n') (h : m + n' = m + n) :
@[simp]
theorem fin.cast_nat_add_left {n m m' : } (i : fin n) (h : m' + n = m + n) :
theorem fin.cast_add_nat_add (p m : ) {n : } (i : fin n) :
theorem fin.nat_add_cast_add (p m : ) {n : } (i : fin n) :
theorem fin.nat_add_nat_add (m n : ) {p : } (i : fin p) :
@[simp]
theorem fin.cast_nat_add_zero {n n' : } (i : fin n) (h : 0 + n = n') :
@[simp]
theorem fin.cast_nat_add (n : ) {m : } (i : fin m) :
@[simp]
theorem fin.cast_add_nat {n : } (m : ) (i : fin n) :
@[simp]
theorem fin.nat_add_last {m n : } :

### pred #

@[simp]
theorem fin.coe_pred {n : } (j : fin (n + 1)) (h : j 0) :
(j.pred h) = j - 1
@[simp]
theorem fin.succ_pred {n : } (i : fin (n + 1)) (h : i 0) :
(i.pred h).succ = i
@[simp]
theorem fin.pred_succ {n : } (i : fin n) {h : i.succ 0} :
i.succ.pred h = i
theorem fin.pred_eq_iff_eq_succ {n : } (i : fin (n + 1)) (hi : i 0) (j : fin n) :
i.pred hi = j i = j.succ
@[simp]
theorem fin.pred_mk_succ {n : } (i : ) (h : i < n + 1) :
i + 1, _⟩.pred _ = i, h⟩
theorem fin.pred_mk {n : } (i : ) (h : i < n + 1) (w : i, h⟩ 0) :
i, h⟩.pred w = i - 1, _⟩
@[simp]
theorem fin.pred_le_pred_iff {n : } {a b : fin n.succ} {ha : a 0} {hb : b 0} :
a.pred ha b.pred hb a b
@[simp]
theorem fin.pred_lt_pred_iff {n : } {a b : fin n.succ} {ha : a 0} {hb : b 0} :
a.pred ha < b.pred hb a < b
@[simp]
theorem fin.pred_inj {n : } {a b : fin (n + 1)} {ha : a 0} {hb : b 0} :
a.pred ha = b.pred hb a = b
@[simp]
theorem fin.pred_one {n : } :
1.pred _ = 0
theorem fin.pred_add_one {n : } (i : fin (n + 2)) (h : i < n + 1) :
(i + 1).pred _ = i.cast_lt h
def fin.sub_nat {n : } (m : ) (i : fin (n + m)) (h : m i) :
fin n

`sub_nat i h` subtracts `m` from `i`, generalizes `fin.pred`.

Equations
@[simp]
theorem fin.coe_sub_nat {n m : } (i : fin (n + m)) (h : m i) :
i h) = i - m
@[simp]
theorem fin.sub_nat_mk {n m i : } (h₁ : i < n + m) (h₂ : m i) :
i, h₁⟩ h₂ = i - m, _⟩
@[simp]
theorem fin.pred_cast_succ_succ {n : } (i : fin n) :
.pred _ =
@[simp]
theorem fin.add_nat_sub_nat {n m : } {i : fin (n + m)} (h : m i) :
(fin.add_nat m) i h) = i
@[simp]
theorem fin.sub_nat_add_nat {n : } (i : fin n) (m : ) (h : m ((fin.add_nat m) i) := _) :
((fin.add_nat m) i) h = i
@[simp]
theorem fin.nat_add_sub_nat_cast {n m : } {i : fin (n + m)} (h : n i) :
(fin.nat_add n) ((fin.cast _) i) h) = i
def fin.div_nat {n m : } (i : fin (m * n)) :
fin m

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

Equations
@[simp]
theorem fin.coe_div_nat {n m : } (i : fin (m * n)) :
(i.div_nat) = i / n
def fin.mod_nat {n m : } (i : fin (m * n)) :
fin n

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

Equations
@[simp]
theorem fin.coe_mod_nat {n m : } (i : fin (m * n)) :
(i.mod_nat) = i % n

### recursion and induction principles #

def fin.succ_rec {C : Π (n : ), fin n Sort u_1} (H0 : Π (n : ), C n.succ 0) (Hs : Π (n : ) (i : fin n), C n i C n.succ i.succ) {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.succ_rec_on {n : } (i : fin n) {C : Π (n : ), fin n Sort u_1} (H0 : Π (n : ), C n.succ 0) (Hs : Π (n : ) (i : fin n), C n i C n.succ i.succ) :
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.succ_rec` taking `i : fin n` as the first argument.

Equations
@[simp]
theorem fin.succ_rec_on_zero {C : Π (n : ), fin n Sort u_1} {H0 : Π (n : ), C n.succ 0} {Hs : Π (n : ) (i : fin n), C n i C n.succ i.succ} (n : ) :
0.succ_rec_on H0 Hs = H0 n
@[simp]
theorem fin.succ_rec_on_succ {C : Π (n : ), fin n Sort u_1} {H0 : Π (n : ), C n.succ 0} {Hs : Π (n : ) (i : fin n), C n i C n.succ i.succ} {n : } (i : fin n) :
i.succ.succ_rec_on H0 Hs = Hs n i (i.succ_rec_on H0 Hs)
def fin.induction {n : } {C : fin (n + 1) Sort u_1} (h0 : C 0) (hs : Π (i : fin n), C C i.succ) (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.cast_succ`.

Equations
• hs = λ (i : fin (n + 1)), i.cases_on (λ (i : ) (hi : i < n + 1), nat.rec (λ (hi : 0 < n + 1), _.mpr h0) (λ (i : ) (IH : Π (hi : i < n + 1), C i, hi⟩) (hi : i.succ < n + 1), hs i, _⟩ (IH _)) i hi)
@[simp]
theorem fin.induction_zero {n : } {C : fin (n + 1) Sort u_1} (h0 : C 0) (hs : Π (i : fin n), C C i.succ) :
hs 0 = h0
@[simp]
theorem fin.induction_succ {n : } {C : fin (n + 1) Sort u_1} (h0 : C 0) (hs : Π (i : fin n), C C i.succ) (i : fin n) :
hs i.succ = hs i hs (fin.cast_succ i))
def fin.induction_on {n : } (i : fin (n + 1)) {C : fin (n + 1) Sort u_1} (h0 : C 0) (hs : Π (i : fin n), C C i.succ) :
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.cast_succ`.

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

Equations
def fin.cases {n : } {C : fin n.succ Sort u_1} (H0 : C 0) (Hs : Π (i : fin n), C i.succ) (i : fin n.succ) :
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.succ Sort u_1} {H0 : C 0} {Hs : Π (i : fin n), C i.succ} :
Hs 0 = H0
@[simp]
theorem fin.cases_succ {n : } {C : fin n.succ Sort u_1} {H0 : C 0} {Hs : Π (i : fin n), C i.succ} (i : fin n) :
Hs i.succ = Hs i
@[simp]
theorem fin.cases_succ' {n : } {C : fin n.succ Sort u_1} {H0 : C 0} {Hs : Π (i : fin n), C i.succ} {i : } (h : i + 1 < n + 1) :
Hs i.succ, h⟩ = Hs i, _⟩
theorem fin.forall_fin_succ {n : } {P : fin (n + 1) Prop} :
( (i : fin (n + 1)), P i) P 0 (i : fin n), P i.succ
theorem fin.exists_fin_succ {n : } {P : fin (n + 1) Prop} :
( (i : fin (n + 1)), P i) P 0 (i : fin n), P i.succ
theorem fin.forall_fin_one {p : fin 1 Prop} :
( (i : fin 1), p i) p 0
theorem fin.exists_fin_one {p : fin 1 Prop} :
( (i : fin 1), p i) p 0
theorem fin.forall_fin_two {p : fin 2 Prop} :
( (i : fin 2), p i) p 0 p 1
theorem fin.exists_fin_two {p : fin 2 Prop} :
( (i : fin 2), p i) p 0 p 1
theorem fin.fin_two_eq_of_eq_zero_iff {a b : fin 2} (h : a = 0 b = 0) :
a = b
def fin.reverse_induction {n : } {C : fin (n + 1) Sort u_1} (hlast : C (fin.last n)) (hs : Π (i : fin n), C i.succ C ) (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
@[simp]
theorem fin.reverse_induction_last {n : } {C : fin (n + 1) Sort u_1} (h0 : C (fin.last n)) (hs : Π (i : fin n), C i.succ C ) :
(fin.last n) = h0
@[simp]
theorem fin.reverse_induction_cast_succ {n : } {C : fin (n + 1) Sort u_1} (h0 : C (fin.last n)) (hs : Π (i : fin n), C i.succ C ) (i : fin n) :
= hs i hs i.succ)
def fin.last_cases {n : } {C : fin (n + 1) Sort u_1} (hlast : C (fin.last n)) (hcast : Π (i : fin n), C ) (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.cast_succ`, `j : fin n`.

Equations
@[simp]
theorem fin.last_cases_last {n : } {C : fin (n + 1) Sort u_1} (hlast : C (fin.last n)) (hcast : Π (i : fin n), C ) :
fin.last_cases hlast hcast (fin.last n) = hlast
@[simp]
theorem fin.last_cases_cast_succ {n : } {C : fin (n + 1) Sort u_1} (hlast : C (fin.last n)) (hcast : Π (i : fin n), C ) (i : fin n) :
fin.last_cases hlast hcast = hcast i
def fin.add_cases {m n : } {C : fin (m + n) Sort u} (hleft : Π (i : fin m), C ((fin.cast_add n) i)) (hright : Π (i : fin n), C ((fin.nat_add m) i)) (i : fin (m + n)) :
C i

Define `f : Π i : fin (m + n), C i` by separately handling the cases `i = cast_add n i`, `j : fin m` and `i = nat_add m j`, `j : fin n`.

Equations
@[simp]
theorem fin.add_cases_left {m n : } {C : fin (m + n) Sort u_1} (hleft : Π (i : fin m), C ((fin.cast_add n) i)) (hright : Π (i : fin n), C ((fin.nat_add m) i)) (i : fin m) :
@[simp]
theorem fin.add_cases_right {m n : } {C : fin (m + n) Sort u_1} (hleft : Π (i : fin m), C ((fin.cast_add n) i)) (hright : Π (i : fin n), C ((fin.nat_add m) i)) (i : fin n) :
theorem fin.lift_fun_iff_succ {n : } {α : Type u_1} (r : α α Prop) [ r] {f : fin (n + 1) α} :
(has_lt.lt r) f f (i : fin n), r (f (fin.cast_succ i)) (f i.succ)
theorem fin.strict_mono_iff_lt_succ {n : } {α : Type u_1} [preorder α] {f : fin (n + 1) α} :
(i : fin n), f < f i.succ

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} [preorder α] {f : fin (n + 1) α} :
(i : fin n), f f i.succ

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

theorem fin.strict_anti_iff_succ_lt {n : } {α : Type u_1} [preorder α] {f : fin (n + 1) α} :
(i : fin n), f i.succ < f

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} [preorder α] {f : fin (n + 1) α} :
(i : fin n), f i.succ f

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

@[protected, instance]
def fin.has_neg (n : ) :

Negation on `fin n`

Equations
@[protected, instance]
def fin.add_comm_group (n : ) [ne_zero n] :

Abelian group structure on `fin n`.

Equations
@[protected, instance]

Note this is more general than `fin.add_comm_group` as it applies (vacuously) to `fin 0` too.

Equations
@[protected, instance]

Note this is more general than `fin.add_comm_group` as it applies (vacuously) to `fin 0` too.

@[protected, instance]

Note this is more general than `fin.add_comm_group` as it applies (vacuously) to `fin 0` too.

Equations
@[protected, instance]

Note this is more general than `fin.add_comm_group` as it applies (vacuously) to `fin 0` too.

Equations
@[protected]
theorem fin.coe_neg {n : } (a : fin n) :
-a = (n - a) % n
@[protected]
theorem fin.coe_sub {n : } (a b : fin n) :
(a - b) = (a + (n - b)) % n
@[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) = ite (a = 0) n (a - 1)
theorem fin.coe_sub_iff_le {n : } {a b : fin n} :
(a - b) = a - b b a
theorem fin.coe_sub_iff_lt {n : } {a 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 =
theorem fin.succ_above_aux {n : } (p : fin (n + 1)) :
strict_mono (λ (i : fin n), ite < p) i.succ)
def fin.succ_above {n : } (p : fin (n + 1)) :
fin n ↪o fin (n + 1)

`succ_above p i` embeds `fin n` into `fin (n + 1)` with a hole around `p`.

Equations
theorem fin.succ_above_below {n : } (p : fin (n + 1)) (i : fin n) (h : < p) :

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

@[simp]
theorem fin.succ_above_ne_zero_zero {n : } [ne_zero n] {a : fin (n + 1)} (ha : a 0) :
theorem fin.succ_above_eq_zero_iff {n : } [ne_zero n] {a : fin (n + 1)} {b : fin n} (ha : a 0) :
(a.succ_above) b = 0 b = 0
theorem fin.succ_above_ne_zero {n : } [ne_zero n] {a : fin (n + 1)} {b : fin n} (ha : a 0) (hb : b 0) :
@[simp]
theorem fin.succ_above_zero {n : } :

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

@[simp]
theorem fin.succ_above_last {n : } :

Embedding `fin n` into `fin (n + 1)` with a hole around `last n` embeds by `cast_succ`.

theorem fin.succ_above_last_apply {n : } (i : fin n) :
theorem fin.succ_above_above {n : } (p : fin (n + 1)) (i : fin n) (h : p ) :

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.succ_above_lt_ge {n : } (p : fin (n + 1)) (i : fin n) :

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

theorem fin.succ_above_lt_gt {n : } (p : fin (n + 1)) (i : fin n) :
p < i.succ

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

@[simp]
theorem fin.succ_above_lt_iff {n : } (p : fin (n + 1)) (i : fin n) :

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_succ_above_iff {n : } (p : fin (n + 1)) (i : fin n) :

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.succ_above_ne {n : } (p : fin (n + 1)) (i : fin n) :

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

theorem fin.succ_above_pos {n : } [ne_zero n] (p : fin (n + 1)) (i : fin n) (h : 0 < i) :

Embedding a positive `fin n` results in a positive fin (n + 1)`

@[simp]
theorem fin.succ_above_cast_lt {n : } {x y : fin (n + 1)} (h : x < y) (hx : x.val < n := _) :
(y.succ_above) (x.cast_lt hx) = x
@[simp]
theorem fin.succ_above_pred {n : } {x y : fin (n + 1)} (h : x < y) (hy : y 0 := _) :
(x.succ_above) (y.pred hy) = y
theorem fin.cast_lt_succ_above {n : } {x : fin n} {y : fin (n + 1)} (h : < y) (h' : ((y.succ_above) x).val < n := _) :
((y.succ_above) x).cast_lt h' = x
theorem fin.pred_succ_above {n : } {x : fin n} {y : fin (n + 1)} (h : y ) (h' : (y.succ_above) x 0 := _) :
((y.succ_above) x).pred h' = x
theorem fin.exists_succ_above_eq {n : } {x y : fin (n + 1)} (h : x y) :
(z : fin n), (y.succ_above) z = x
@[simp]
theorem fin.exists_succ_above_eq_iff {n : } {x y : fin (n + 1)} :
( (z : fin n), (x.succ_above) z = y) y x
@[simp]
theorem fin.range_succ_above {n : } (p : fin (n + 1)) :
= {p}

The range of `p.succ_above` is everything except `p`.

@[simp]
theorem fin.range_succ (n : ) :
@[simp]
theorem fin.exists_succ_eq_iff {n : } {x : fin (n + 1)} :
( (y : fin n), y.succ = x) x 0
theorem fin.succ_above_right_injective {n : } {x : fin (n + 1)} :

Given a fixed pivot `x : fin (n + 1)`, `x.succ_above` is injective

theorem fin.succ_above_right_inj {n : } {a b : fin n} {x : fin (n + 1)} :

Given a fixed pivot `x : fin (n + 1)`, `x.succ_above` is injective

`succ_above` is injective at the pivot

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

`succ_above` is injective at the pivot

@[simp]
theorem fin.zero_succ_above {n : } (i : fin n) :
@[simp]
theorem fin.succ_succ_above_zero {n : } [ne_zero n] (i : fin n) :
@[simp]
theorem fin.succ_succ_above_succ {n : } (i : fin (n + 1)) (j : fin n) :
@[simp]
theorem fin.one_succ_above_zero {n : } :
@[simp]
theorem fin.succ_succ_above_one {n : } [ne_zero n] (i : fin (n + 1)) :

By moving `succ` to the outside of this expression, we create opportunities for further simplification using `succ_above_zero` or `succ_succ_above_zero`.

@[simp]
theorem fin.one_succ_above_succ {n : } (j : fin n) :
@[simp]
theorem fin.one_succ_above_one {n : } :
def fin.pred_above {n : } (p : fin n) (i : fin (n + 1)) :
fin n

`pred_above p i` embeds `i : fin (n+1)` into `fin n` by subtracting one if `p < i`.

Equations
theorem fin.pred_above_right_monotone {n : } (p : fin n) :
theorem fin.pred_above_left_monotone {n : } (i : fin (n + 1)) :
monotone (λ (p : fin n), p.pred_above i)
def fin.cast_pred {n : } (i : fin (n + 2)) :
fin (n + 1)

`cast_pred` embeds `i : fin (n + 2)` into `fin (n + 1)` by lowering just `last (n + 1)` to `last n`.

Equations
@[simp]
theorem fin.cast_pred_zero {n : } :
@[simp]
theorem fin.cast_pred_one {n : } :
@[simp]
theorem fin.pred_above_zero {n : } {i : fin (n + 2)} (hi : i 0) :
0.pred_above i = i.pred hi
@[simp]
theorem fin.cast_pred_last {n : } :
@[simp]
theorem fin.cast_pred_mk (n i : ) (h : i < n + 1) :
i, _⟩.cast_pred = i, h⟩
theorem fin.coe_cast_pred {n : } (a : fin (n + 2)) (hx : a < fin.last (n + 1)) :
theorem fin.pred_above_below {n : } (p : fin (n + 1)) (i : fin (n + 2)) (h : i ) :
@[simp]
theorem fin.pred_above_last {n : } :
theorem fin.pred_above_above {n : } (p : fin n) (i : fin (n + 1)) (h : < i) :
p.pred_above i = i.pred _
theorem fin.cast_pred_monotone {n : } :
@[simp]
theorem fin.succ_above_pred_above {n : } {p : fin n} {i : fin (n + 1)} (h : 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.pred_above_succ_above {n : } (p i : fin n) :

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.cast_succ_pred_eq_pred_cast_succ {n : } {a : fin (n + 1)} (ha : a 0) (ha' : := _) :
theorem fin.pred_succ_above_pred {n : } {a : fin (n + 2)} {b : fin (n + 1)} (ha : a 0) (hb : b 0) (hk : (a.succ_above) b 0 := _) :
((a.pred ha).succ_above) (b.pred hb) = ((a.succ_above) b).pred hk

`pred` commutes with `succ_above`.

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

`succ` commutes with `pred_above`.

@[simp]
theorem fin.cast_pred_cast_succ {n : } (i : fin (n + 1)) :
= i
theorem fin.cast_succ_cast_pred {n : } {i : fin (n + 2)} (h : i < fin.last (n + 1)) :
theorem fin.coe_cast_pred_le_self {n : } (i : fin (n + 2)) :
theorem fin.coe_cast_pred_lt_iff {n : } {i : fin (n + 2)} :
theorem fin.lt_last_iff_coe_cast_pred {n : } {i : fin (n + 2)} :
def fin.clamp (n m : ) :
fin (m + 1)

`min n m` as an element of `fin (m + 1)`

Equations
• m =
@[simp]
theorem fin.coe_clamp (n m : ) :
m) =
@[simp]
theorem fin.coe_of_nat_eq_mod (m n : ) [ne_zero m] :
n = n % m

### mul #

theorem fin.val_mul {n : } (a b : fin n) :
(a * b).val = a.val * b.val % n
theorem fin.coe_mul {n : } (a b : fin n) :
(a * b) = a * b % n
@[protected, simp]
theorem fin.mul_one {n : } [ne_zero n] (k : fin n) :
k * 1 = k
@[protected]
theorem fin.mul_comm {n : } (a b : fin n) :
a * b = b * a
@[protected, simp]
theorem fin.one_mul {n : } [ne_zero n] (k : fin n) :
1 * k = k
@[protected, simp]
theorem fin.mul_zero {n : } [ne_zero n] (k : fin n) :
k * 0 = 0
@[protected, simp]
theorem fin.zero_mul {n : } [ne_zero n] (k : fin n) :
0 * k = 0
@[protected, instance]
meta def fin.reflect (n : ) :