mathlib3 documentation

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 #

Order embeddings and an order isomorphism #

Other casts #

Misc definitions #

source
def fin_zero_elim {α : fin 0 → Sort u} (x : fin 0) :
α x

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

Equations
source
def fin.elim0' {α : Sort u_1} (x : fin 0) :
α

A non-dependent variant of elim0.

Equations
source
@[protected, instance]
def fin.fin_to_nat (n : ℕ) :
has_coe (fin n) ℕ
Equations
source
theorem fin.val_injective {n : ℕ} :
function.injective fin.val
source
@[protected]
theorem fin.prop {n : ℕ} (a : fin n) :
a.val < n
source
@[simp]
theorem fin.is_lt {n : ℕ} (a : fin n) :
↑a < n
source
@[protected]
theorem fin.pos {n : ℕ} (i : fin n) :
0 < n
source
theorem fin.pos_iff_nonempty {n : ℕ} :
0 < n ↔ nonempty (fin n)
source
def fin.equiv_subtype {n : ℕ} :
fin n ≃ {i // i < n}

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

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

coercions and constructions #

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

source
@[protected]
theorem fin.heq_ext_iff {k l : ℕ} (h : k = l) {i : fin k} {j : fin l} :
i == j ↔ ↑i = ↑j
source
theorem fin.exists_iff {n : ℕ} {p : fin n → Prop} :
(∃ (i : fin n), p i) ↔ ∃ (i : ℕ) (h : i < n), p ⟨i, h⟩
source
theorem fin.forall_iff {n : ℕ} {p : fin n → Prop} :
(∀ (i : fin n), p i) ↔ ∀ (i : ℕ) (h : i < n), p ⟨i, h⟩

order #

source
theorem fin.is_le {n : ℕ} (i : fin (n + 1)) :
↑i ≤ n
source
@[simp]
theorem fin.is_le' {n : ℕ} {a : fin n} :
↑a ≤ n
source
theorem fin.lt_iff_coe_lt_coe {n : ℕ} {a b : fin n} :
a < b ↔ ↑a < ↑b
source
theorem fin.le_iff_coe_le_coe {n : ℕ} {a b : fin n} :
a ≤ b ↔ ↑a ≤ ↑b
source
theorem fin.mk_lt_of_lt_coe {n : ℕ} {b : fin n} {a : ℕ} (h : a < ↑b) :
⟨a, _⟩ < b
source
theorem fin.mk_le_of_le_coe {n : ℕ} {b : fin n} {a : ℕ} (h : a ≤ ↑b) :
⟨a, _⟩ ≤ b
source
@[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.

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

source
@[protected, instance]
def fin.linear_order {n : ℕ} :
linear_order (fin n)
Equations
source
@[simp]
theorem fin.mk_le_mk {n x y : ℕ} {hx : x < n} {hy : y < n} :
⟨x, hx⟩ ≤ ⟨y, hy⟩ ↔ x ≤ y
source
@[simp]
theorem fin.mk_lt_mk {n x y : ℕ} {hx : x < n} {hy : y < n} :
⟨x, hx⟩ < ⟨y, hy⟩ ↔ x < y
source
@[simp]
theorem fin.min_coe {n : ℕ} {a : fin n} :
linear_order.min ↑a n = ↑a
source
@[simp]
theorem fin.max_coe {n : ℕ} {a : fin n} :
linear_order.max ↑a n = n
source
@[protected, instance]
def fin.partial_order {n : ℕ} :
partial_order (fin n)
Equations
source
theorem fin.coe_strict_mono {n : ℕ} :
strict_mono coe
source
def fin.order_iso_subtype {n : ℕ} :
fin n ≃o {i // i < n}

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

Equations
source
@[simp]
theorem fin.order_iso_subtype_apply {n : ℕ} (a : fin n) :
⇑fin.order_iso_subtype a = ⟨↑a, _⟩
source
@[simp]
theorem fin.order_iso_subtype_symm_apply {n : ℕ} (a : {i // i < n}) :
⇑(rel_iso.symm fin.order_iso_subtype) a = ⟨↑a, _⟩
source
def fin.coe_embedding {n : ℕ} :
fin n ↪ ℕ

The inclusion map fin n → ℕ is an embedding.

Equations
source
@[simp]
theorem fin.coe_embedding_apply {n : ℕ} (ᾰ : fin n) :
⇑fin.coe_embedding ᾰ = ↑ᾰ
source
@[simp]
theorem fin.equiv_subtype_symm_trans_val_embedding {n : ℕ} :
fin.equiv_subtype.symm.to_embedding.trans fin.coe_embedding = function.embedding.subtype (λ (_x : ℕ), _x < n)
source
@[simp]
theorem fin.coe_order_embedding_apply (n : ℕ) (ᾰ : fin n) :
⇑(fin.coe_order_embedding n) ᾰ = ↑ᾰ
source
def fin.coe_order_embedding (n : ℕ) :
fin n ↪o ℕ

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

Equations
source
@[protected, instance]
def fin.fin.lt.is_well_order (n : ℕ) :
is_well_order (fin n) has_lt.lt

The ordering on fin n is a well order.

source
@[protected, instance]
def fin.has_well_founded {n : ℕ} :
has_well_founded (fin n)

Use the ordering on fin n for checking recursive definitions.

For example, the following definition is not accepted by the termination checker, unless we declare the 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
source
@[protected, instance]
def fin.has_zero_of_ne_zero {n : ℕ} [ne_zero n] :
has_zero (fin n)
Equations
source
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
source
@[protected, instance]
def fin.has_one_of_ne_zero {n : ℕ} [ne_zero n] :
has_one (fin n)
Equations
source
@[simp]
theorem fin.coe_zero (n : ℕ) [ne_zero n] :
↑0 = 0
source
@[simp]
theorem fin.val_zero' (n : ℕ) [ne_zero n] :
0.val = 0
source
@[simp]
theorem fin.mk_zero {n : ℕ} [ne_zero n] :
⟨0, _⟩ = 0
source
@[simp]
theorem fin.zero_le {n : ℕ} [ne_zero n] (a : fin n) :
0 ≤ a
source
theorem fin.zero_lt_one {n : ℕ} :
0 < 1
source
@[simp]
theorem fin.not_lt_zero {n : ℕ} (a : fin n.succ) :
¬a < 0
source
theorem fin.pos_iff_ne_zero {n : ℕ} [ne_zero n] (a : fin n) :
0 < a ↔ a ≠ 0
source
theorem fin.eq_zero_or_eq_succ {n : ℕ} (i : fin (n + 1)) :
i = 0 ∨ ∃ (j : fin n), i = j.succ
source
theorem fin.eq_succ_of_ne_zero {n : ℕ} {i : fin (n + 1)} (hi : i ≠ 0) :
∃ (j : fin n), i = j.succ
source
def fin.rev {n : ℕ} :
equiv.perm (fin n)

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

Equations
source
@[simp]
theorem fin.coe_rev {n : ℕ} (i : fin n) :
↑(⇑fin.rev i) = n - (↑i + 1)
source
theorem fin.rev_involutive {n : ℕ} :
function.involutive ⇑fin.rev
source
theorem fin.rev_injective {n : ℕ} :
function.injective ⇑fin.rev
source
theorem fin.rev_surjective {n : ℕ} :
function.surjective ⇑fin.rev
source
theorem fin.rev_bijective {n : ℕ} :
function.bijective ⇑fin.rev
source
@[simp]
theorem fin.rev_inj {n : ℕ} {i j : fin n} :
⇑fin.rev i = ⇑fin.rev j ↔ i = j
source
@[simp]
theorem fin.rev_rev {n : ℕ} (i : fin n) :
⇑fin.rev (⇑fin.rev i) = i
source
@[simp]
theorem fin.rev_symm {n : ℕ} :
equiv.symm fin.rev = fin.rev
source
theorem fin.rev_eq {n a : ℕ} (i : fin (n + 1)) (h : n = a + ↑i) :
⇑fin.rev i = ⟨a, _⟩
source
@[simp]
theorem fin.rev_le_rev {n : ℕ} {i j : fin n} :
⇑fin.rev i ≤ ⇑fin.rev j ↔ j ≤ i
source
@[simp]
theorem fin.rev_lt_rev {n : ℕ} {i j : fin n} :
⇑fin.rev i < ⇑fin.rev j ↔ j < i
source
@[simp]
theorem fin.rev_order_iso_apply {n : ℕ} (ᾰ : (fin n)ᵒᵈ) :
⇑fin.rev_order_iso ᾰ = ⇑fin.rev (⇑order_dual.of_dual ᾰ)
source
def fin.rev_order_iso {n : ℕ} :
(fin n)ᵒᵈ ≃o fin n

fin.rev n as an order-reversing isomorphism.

Equations
source
@[simp]
theorem fin.rev_order_iso_to_equiv {n : ℕ} :
fin.rev_order_iso.to_equiv = order_dual.of_dual.trans fin.rev
source
@[simp]
theorem fin.rev_order_iso_symm_apply {n : ℕ} (i : fin n) :
⇑(fin.rev_order_iso.symm) i = ⇑order_dual.to_dual (⇑fin.rev i)
source
def fin.last (n : ℕ) :
fin (n + 1)

The greatest value of fin (n+1)

Equations
source
@[simp, norm_cast]
theorem fin.coe_last (n : ℕ) :
↑(fin.last n) = n
source
theorem fin.last_val (n : ℕ) :
(fin.last n).val = n
source
theorem fin.le_last {n : ℕ} (i : fin (n + 1)) :
i ≤ fin.last n
source
@[protected, instance]
def fin.bounded_order {n : ℕ} :
bounded_order (fin (n + 1))
Equations
source
@[protected, instance]
def fin.lattice {n : ℕ} :
lattice (fin (n + 1))
Equations
source
theorem fin.last_pos {n : ℕ} :
0 < fin.last (n + 1)
source
theorem fin.eq_last_of_not_lt {n : ℕ} {i : fin (n + 1)} (h : ¬↑i < n) :
i = fin.last n
source
theorem fin.top_eq_last (n : ℕ) :
⊤ = fin.last n
source
theorem fin.bot_eq_zero (n : ℕ) :
⊥ = 0
source
@[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 : ℕ).

source
@[protected, instance]
def fin.order_iso_subsingleton {n : ℕ} {α : Type u_1} [preorder α] :
subsingleton (fin n ≃o α)
source
@[protected, instance]
def fin.order_iso_subsingleton' {n : ℕ} {α : Type u_1} [preorder α] :
subsingleton (α ≃o fin n)
source
@[protected, instance]
def fin.order_iso_unique {n : ℕ} :
unique (fin n ≃o fin n)
Equations
source
theorem fin.strict_mono_unique {n : ℕ} {α : Type u_1} [preorder α] {f g : fin n → α} (hf : strict_mono f) (hg : strict_mono g) (h : set.range f = set.range g) :
f = g

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

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

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

addition, numerals, and coercion from nat #

source
theorem fin.one_val {n : ℕ} :
1.val = 1 % (n + 1)
source
theorem fin.coe_one' (n : ℕ) [ne_zero n] :
↑1 = 1 % n
source
@[simp]
theorem fin.val_one (n : ℕ) :
1.val = 1
source
@[simp]
theorem fin.coe_one (n : ℕ) :
↑1 = 1
source
@[simp]
theorem fin.mk_one {n : ℕ} :
⟨1, _⟩ = 1
source
@[protected, instance]
def fin.nontrivial {n : ℕ} :
nontrivial (fin (n + 2))
source
theorem fin.nontrivial_iff_two_le {n : ℕ} :
nontrivial (fin n) ↔ 2 ≤ n
source
theorem fin.subsingleton_iff_le_one {n : ℕ} :
subsingleton (fin n) ↔ n ≤ 1
source
@[protected, instance]
def fin.add_comm_semigroup (n : ℕ) :
add_comm_semigroup (fin n)
Equations
source
@[protected, simp]
theorem fin.add_zero {n : ℕ} [ne_zero n] (k : fin n) :
k + 0 = k
source
@[protected, simp]
theorem fin.zero_add {n : ℕ} [ne_zero n] (k : fin n) :
0 + k = k
source
@[protected, instance]
def fin.add_comm_monoid (n : ℕ) [ne_zero n] :
add_comm_monoid (fin n)
Equations
source
@[protected, instance]
def fin.add_monoid_with_one {n : ℕ} [ne_zero n] :
add_monoid_with_one (fin n)
Equations
source
theorem fin.val_add {n : ℕ} (a b : fin n) :
(a + b).val = (a.val + b.val) % n
source
theorem fin.coe_add {n : ℕ} (a b : fin n) :
↑(a + b) = (↑a + ↑b) % n
source
theorem fin.coe_add_eq_ite {n : ℕ} (a b : fin n) :
↑(a + b) = ite (n ≤ ↑a + ↑b) (↑a + ↑b - n) (↑a + ↑b)
source
theorem fin.coe_bit0 {n : ℕ} (k : fin n) :
↑(bit0 k) = bit0 ↑k % n
source
theorem fin.coe_bit1 {n : ℕ} [ne_zero n] (k : fin n) :
↑(bit1 k) = bit1 ↑k % n
source
theorem fin.coe_add_one_of_lt {n : ℕ} {i : fin n.succ} (h : i < fin.last n) :
↑(i + 1) = ↑i + 1
source
@[simp]
theorem fin.last_add_one (n : ℕ) :
fin.last n + 1 = 0
source
theorem fin.coe_add_one {n : ℕ} (i : fin (n + 1)) :
↑(i + 1) = ite (i = fin.last n) 0 (↑i + 1)
source
@[simp]
theorem fin.mk_bit0 {m n : ℕ} (h : bit0 m < n) :
⟨bit0 m, h⟩ = bit0 ⟨m, _⟩
source
@[simp]
theorem fin.mk_bit1 {m n : ℕ} [ne_zero n] (h : bit1 m < n) :
⟨bit1 m, h⟩ = bit1 ⟨m, _⟩
source
@[simp]
theorem fin.val_two {n : ℕ} :
2.val = 2
source
@[simp]
theorem fin.coe_two {n : ℕ} :
↑2 = 2
source
@[simp]
theorem fin.of_nat_eq_coe (n a : ℕ) :
fin.of_nat a = ↑a
source
@[simp]
theorem fin.of_nat'_eq_coe (n : ℕ) [ne_zero n] (a : ℕ) :
fin.of_nat' a = ↑a
source
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.

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

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

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

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

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

source
theorem fin.coe_nat_eq_last (n : ℕ) :
↑n = fin.last n
source
theorem fin.le_coe_last {n : ℕ} (i : fin (n + 1)) :
i ≤ ↑n
source
theorem fin.add_one_pos {n : ℕ} (i : fin (n + 1)) (h : i < fin.last n) :
0 < i + 1
source
theorem fin.one_pos {n : ℕ} :
0 < 1
source
theorem fin.zero_ne_one {n : ℕ} :
0 ≠ 1
source
@[simp]
theorem fin.zero_eq_one_iff {n : ℕ} [ne_zero n] :
0 = 1 ↔ n = 1
source
@[simp]
theorem fin.one_eq_zero_iff {n : ℕ} [ne_zero n] :
1 = 0 ↔ n = 1

succ and casts into larger fin types #

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

fin.succ as an order_embedding

Equations
source
@[simp]
theorem fin.coe_succ_embedding {n : ℕ} :
⇑(fin.succ_embedding n) = fin.succ
source
@[simp]
theorem fin.succ_le_succ_iff {n : ℕ} {a b : fin n} :
a.succ ≤ b.succ ↔ a ≤ b
source
@[simp]
theorem fin.succ_lt_succ_iff {n : ℕ} {a b : fin n} :
a.succ < b.succ ↔ a < b
source
theorem fin.succ_injective (n : ℕ) :
function.injective fin.succ
source
@[simp]
theorem fin.succ_inj {n : ℕ} {a b : fin n} :
a.succ = b.succ ↔ a = b
source
theorem fin.succ_ne_zero {n : ℕ} (k : fin n) :
k.succ ≠ 0
source
@[simp]
theorem fin.succ_zero_eq_one {n : ℕ} [ne_zero n] :
0.succ = 1
source
@[simp]
theorem fin.succ_zero_eq_one' {n : ℕ} :
0.succ = 1

Version of succ_zero_eq_one to be used by dsimp

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

Version of succ_one_eq_two to be used by dsimp

source
@[simp]
theorem fin.succ_mk (n i : ℕ) (h : i < n) :
⟨i, h⟩.succ = ⟨i + 1, _⟩
source
theorem fin.mk_succ_pos {n : ℕ} (i : ℕ) (h : i < n) :
0 < ⟨i.succ, _⟩
source
theorem fin.one_lt_succ_succ {n : ℕ} (a : fin n) :
1 < a.succ.succ
source
@[simp]
theorem fin.add_one_lt_iff {n : ℕ} {k : fin (n + 2)} :
k + 1 < k ↔ k = fin.last (n + 1)
source
@[simp]
theorem fin.add_one_le_iff {n : ℕ} {k : fin (n + 1)} :
k + 1 ≤ k ↔ k = fin.last n
source
@[simp]
theorem fin.last_le_iff {n : ℕ} {k : fin (n + 1)} :
fin.last n ≤ k ↔ k = fin.last n
source
@[simp]
theorem fin.lt_add_one_iff {n : ℕ} {k : fin (n + 1)} :
k < k + 1 ↔ k < fin.last n
source
@[simp]
theorem fin.le_zero_iff {n : ℕ} [ne_zero n] {k : fin n} :
k ≤ 0 ↔ k = 0
source
theorem fin.succ_succ_ne_one {n : ℕ} (a : fin n) :
a.succ.succ ≠ 1
source
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
source
@[simp]
theorem fin.coe_cast_lt {n m : ℕ} (i : fin m) (h : i.val < n) :
↑(i.cast_lt h) = ↑i
source
@[simp]
theorem fin.cast_lt_mk (i n m : ℕ) (hn : i < n) (hm : i < m) :
⟨i, hn⟩.cast_lt hm = ⟨i, hm⟩
source
def fin.cast_le {n m : ℕ} (h : n ≤ m) :
fin n ↪o fin m

cast_le h i embeds i into a larger fin type.

Equations
source
@[simp]
theorem fin.coe_cast_le {n m : ℕ} (h : n ≤ m) (i : fin n) :
↑(⇑(fin.cast_le h) i) = ↑i
source
@[simp]
theorem fin.cast_le_mk (i n m : ℕ) (hn : i < n) (h : n ≤ m) :
⇑(fin.cast_le h) ⟨i, hn⟩ = ⟨i, _⟩
source
@[simp]
theorem fin.cast_le_zero {n m : ℕ} (h : n.succ ≤ m.succ) :
⇑(fin.cast_le h) 0 = 0
source
@[simp]
theorem fin.range_cast_le {n k : ℕ} (h : n ≤ k) :
set.range ⇑(fin.cast_le h) = {i : fin k | ↑i < n}
source
@[simp]
theorem fin.coe_of_injective_cast_le_symm {n k : ℕ} (h : n ≤ k) (i : fin k) (hi : i ∈ set.range ⇑(fin.cast_le h)) :
↑(⇑((equiv.of_injective ⇑(fin.cast_le h) _).symm) ⟨i, hi⟩) = ↑i
source
@[simp]
theorem fin.cast_le_succ {m n : ℕ} (h : m + 1 ≤ n + 1) (i : fin m) :
⇑(fin.cast_le h) i.succ = (⇑(fin.cast_le _) i).succ
source
@[simp]
theorem fin.cast_le_cast_le {k m n : ℕ} (km : k ≤ m) (mn : m ≤ n) (i : fin k) :
⇑(fin.cast_le mn) (⇑(fin.cast_le km) i) = ⇑(fin.cast_le _) i
source
@[simp]
theorem fin.cast_le_comp_cast_le {k m n : ℕ} (km : k ≤ m) (mn : m ≤ n) :
⇑(fin.cast_le mn) ∘ ⇑(fin.cast_le km) = ⇑(fin.cast_le _)
source
def fin.cast {n m : ℕ} (eq : n = m) :
fin n ≃o fin m

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

Equations
source
@[simp]
theorem fin.symm_cast {n m : ℕ} (h : n = m) :
(fin.cast h).symm = fin.cast _
source
@[simp]
theorem fin.coe_cast {n m : ℕ} (h : n = m) (i : fin n) :
↑(⇑(fin.cast h) i) = ↑i

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

source
@[simp]
theorem fin.cast_zero {n n' : ℕ} [ne_zero n] {h : n = n'} :
⇑(fin.cast h) 0 = 0
source
@[simp]
theorem fin.cast_last {n n' : ℕ} {h : n + 1 = n' + 1} :
⇑(fin.cast h) (fin.last n) = fin.last n'
source
@[simp]
theorem fin.cast_mk {n m : ℕ} (h : n = m) (i : ℕ) (hn : i < n) :
⇑(fin.cast h) ⟨i, hn⟩ = ⟨i, _⟩
source
@[simp]
theorem fin.cast_trans {n m k : ℕ} (h : n = m) (h' : m = k) {i : fin n} :
⇑(fin.cast h') (⇑(fin.cast h) i) = ⇑(fin.cast _) i
source
@[simp]
theorem fin.cast_refl {n : ℕ} (h : n = n := rfl) :
fin.cast h = order_iso.refl (fin n)
source
theorem fin.cast_le_of_eq {m n : ℕ} (h : m = n) {h' : m ≤ n} :
⇑(fin.cast_le h') = ⇑(fin.cast h)
source
theorem fin.cast_to_equiv {n m : ℕ} (h : n = m) :
(fin.cast h).to_equiv = equiv.cast _

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

source
theorem fin.cast_eq_cast {n m : ℕ} (h : n = m) :
⇑(fin.cast h) = cast _

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

source
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
source
@[simp]
theorem fin.coe_cast_add {n : ℕ} (m : ℕ) (i : fin n) :
↑(⇑(fin.cast_add m) i) = ↑i
source
@[simp]
theorem fin.cast_add_zero {n : ℕ} :
⇑(fin.cast_add 0) = ⇑(fin.cast rfl)
source
theorem fin.cast_add_lt {m : ℕ} (n : ℕ) (i : fin m) :
↑(⇑(fin.cast_add n) i) < m
source
@[simp]
theorem fin.cast_add_mk {n : ℕ} (m i : ℕ) (h : i < n) :
⇑(fin.cast_add m) ⟨i, h⟩ = ⟨i, _⟩
source
@[simp]
theorem fin.cast_add_cast_lt {n : ℕ} (m : ℕ) (i : fin (n + m)) (hi : i.val < n) :
⇑(fin.cast_add m) (i.cast_lt hi) = i
source
@[simp]
theorem fin.cast_lt_cast_add {n : ℕ} (m : ℕ) (i : fin n) :
(⇑(fin.cast_add m) i).cast_lt _ = i
source
theorem fin.cast_add_cast {n n' : ℕ} (m : ℕ) (i : fin n') (h : n' = n) :
⇑(fin.cast_add m) (⇑(fin.cast h) i) = ⇑(fin.cast _) (⇑(fin.cast_add m) i)

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

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

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

source
theorem fin.succ_cast_eq {n n' : ℕ} (i : fin n) (h : n = n') :
(⇑(fin.cast h) i).succ = ⇑(fin.cast _) i.succ
source
def fin.cast_succ {n : ℕ} :
fin n ↪o fin (n + 1)

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

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

cast_succ i is positive when i is positive

source
@[simp]
theorem fin.cast_succ_eq_zero_iff {n : ℕ} [ne_zero n] (a : fin n) :
⇑fin.cast_succ a = 0 ↔ a = 0
source
theorem fin.cast_succ_ne_zero_iff {n : ℕ} [ne_zero n] (a : fin n) :
⇑fin.cast_succ a ≠ 0 ↔ a ≠ 0
source
theorem fin.cast_succ_fin_succ (n : ℕ) (j : fin n) :
⇑fin.cast_succ j.succ = (⇑fin.cast_succ j).succ
source
@[simp, norm_cast]
theorem fin.coe_eq_cast_succ {n : ℕ} {a : fin n} :
↑a = ⇑fin.cast_succ a
source
@[simp]
theorem fin.coe_succ_eq_succ {n : ℕ} {a : fin n} :
⇑fin.cast_succ a + 1 = a.succ
source
theorem fin.lt_succ {n : ℕ} {a : fin n} :
⇑fin.cast_succ a < a.succ
source
@[simp]
theorem fin.range_cast_succ {n : ℕ} :
set.range ⇑fin.cast_succ = {i : fin (n + 1) | ↑i < n}
source
@[simp]
theorem fin.coe_of_injective_cast_succ_symm {n : ℕ} (i : fin (n + 1)) (hi : i ∈ set.range ⇑fin.cast_succ) :
↑(⇑((equiv.of_injective ⇑fin.cast_succ _).symm) ⟨i, hi⟩) = ↑i
source
theorem fin.succ_cast_succ {n : ℕ} (i : fin n) :
(⇑fin.cast_succ i).succ = ⇑fin.cast_succ i.succ
source
def fin.add_nat {n : ℕ} (m : ℕ) :
fin n ↪o fin (n + m)

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

Equations
source
@[simp]
theorem fin.coe_add_nat {n : ℕ} (m : ℕ) (i : fin n) :
↑(⇑(fin.add_nat m) i) = ↑i + m
source
@[simp]
theorem fin.add_nat_one {n : ℕ} {i : fin n} :
⇑(fin.add_nat 1) i = i.succ
source
theorem fin.le_coe_add_nat {n : ℕ} (m : ℕ) (i : fin n) :
m ≤ ↑(⇑(fin.add_nat m) i)
source
@[simp]
theorem fin.add_nat_mk {m : ℕ} (n i : ℕ) (hi : i < m) :
⇑(fin.add_nat n) ⟨i, hi⟩ = ⟨i + n, _⟩
source
@[simp]
theorem fin.cast_add_nat_zero {n n' : ℕ} (i : fin n) (h : n + 0 = n') :
⇑(fin.cast h) (⇑(fin.add_nat 0) i) = ⇑(fin.cast _) i
source
theorem fin.add_nat_cast {n n' m : ℕ} (i : fin n') (h : n' = n) :
⇑(fin.add_nat m) (⇑(fin.cast h) i) = ⇑(fin.cast _) (⇑(fin.add_nat m) i)

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

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

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

Equations
source
@[simp]
theorem fin.coe_nat_add (n : ℕ) {m : ℕ} (i : fin m) :
↑(⇑(fin.nat_add n) i) = n + ↑i
source
@[simp]
theorem fin.nat_add_mk {m : ℕ} (n i : ℕ) (hi : i < m) :
⇑(fin.nat_add n) ⟨i, hi⟩ = ⟨n + i, _⟩
source
theorem fin.le_coe_nat_add {n : ℕ} (m : ℕ) (i : fin n) :
m ≤ ↑(⇑(fin.nat_add m) i)
source
theorem fin.nat_add_zero {n : ℕ} :
fin.nat_add 0 = rel_iso.to_rel_embedding (fin.cast _)
source
theorem fin.nat_add_cast {n n' : ℕ} (m : ℕ) (i : fin n') (h : n' = n) :
⇑(fin.nat_add m) (⇑(fin.cast h) i) = ⇑(fin.cast _) (⇑(fin.nat_add m) i)

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

source
theorem fin.cast_nat_add_right {n n' m : ℕ} (i : fin n') (h : m + n' = m + n) :
⇑(fin.cast h) (⇑(fin.nat_add m) i) = ⇑(fin.nat_add m) (⇑(fin.cast _) i)
source
@[simp]
theorem fin.cast_nat_add_left {n m m' : ℕ} (i : fin n) (h : m' + n = m + n) :
⇑(fin.cast h) (⇑(fin.nat_add m') i) = ⇑(fin.nat_add m) i
source
theorem fin.cast_add_nat_add (p m : ℕ) {n : ℕ} (i : fin n) :
⇑(fin.cast_add p) (⇑(fin.nat_add m) i) = ⇑(fin.cast _) (⇑(fin.nat_add m) (⇑(fin.cast_add p) i))
source
theorem fin.nat_add_cast_add (p m : ℕ) {n : ℕ} (i : fin n) :
⇑(fin.nat_add m) (⇑(fin.cast_add p) i) = ⇑(fin.cast _) (⇑(fin.cast_add p) (⇑(fin.nat_add m) i))
source
theorem fin.nat_add_nat_add (m n : ℕ) {p : ℕ} (i : fin p) :
⇑(fin.nat_add m) (⇑(fin.nat_add n) i) = ⇑(fin.cast _) (⇑(fin.nat_add (m + n)) i)
source
@[simp]
theorem fin.cast_nat_add_zero {n n' : ℕ} (i : fin n) (h : 0 + n = n') :
⇑(fin.cast h) (⇑(fin.nat_add 0) i) = ⇑(fin.cast _) i
source
@[simp]
theorem fin.cast_nat_add (n : ℕ) {m : ℕ} (i : fin m) :
⇑(fin.cast _) (⇑(fin.nat_add n) i) = ⇑(fin.add_nat n) i
source
@[simp]
theorem fin.cast_add_nat {n : ℕ} (m : ℕ) (i : fin n) :
⇑(fin.cast _) (⇑(fin.add_nat m) i) = ⇑(fin.nat_add m) i
source
@[simp]
theorem fin.nat_add_last {m n : ℕ} :
⇑(fin.nat_add n) (fin.last m) = fin.last (n + m)
source
theorem fin.nat_add_cast_succ {m n : ℕ} {i : fin m} :
⇑(fin.nat_add n) (⇑fin.cast_succ i) = ⇑fin.cast_succ (⇑(fin.nat_add n) i)

pred #

source
@[simp]
theorem fin.coe_pred {n : ℕ} (j : fin (n + 1)) (h : j ≠ 0) :
↑(j.pred h) = ↑j - 1
source
@[simp]
theorem fin.succ_pred {n : ℕ} (i : fin (n + 1)) (h : i ≠ 0) :
(i.pred h).succ = i
source
@[simp]
theorem fin.pred_succ {n : ℕ} (i : fin n) {h : i.succ ≠ 0} :
i.succ.pred h = i
source
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
source
@[simp]
theorem fin.pred_mk_succ {n : ℕ} (i : ℕ) (h : i < n + 1) :
⟨i + 1, _⟩.pred _ = ⟨i, h⟩
source
theorem fin.pred_mk {n : ℕ} (i : ℕ) (h : i < n + 1) (w : ⟨i, h⟩ ≠ 0) :
⟨i, h⟩.pred w = ⟨i - 1, _⟩
source
@[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
source
@[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
source
@[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
source
@[simp]
theorem fin.pred_one {n : ℕ} :
1.pred _ = 0
source
theorem fin.pred_add_one {n : ℕ} (i : fin (n + 2)) (h : ↑i < n + 1) :
(i + 1).pred _ = i.cast_lt h
source
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
source
@[simp]
theorem fin.coe_sub_nat {n m : ℕ} (i : fin (n + m)) (h : m ≤ ↑i) :
↑(fin.sub_nat m i h) = ↑i - m
source
@[simp]
theorem fin.sub_nat_mk {n m i : ℕ} (h₁ : i < n + m) (h₂ : m ≤ i) :
fin.sub_nat m ⟨i, h₁⟩ h₂ = ⟨i - m, _⟩
source
@[simp]
theorem fin.pred_cast_succ_succ {n : ℕ} (i : fin n) :
(⇑fin.cast_succ i.succ).pred _ = ⇑fin.cast_succ i
source
@[simp]
theorem fin.add_nat_sub_nat {n m : ℕ} {i : fin (n + m)} (h : m ≤ ↑i) :
⇑(fin.add_nat m) (fin.sub_nat m i h) = i
source
@[simp]
theorem fin.sub_nat_add_nat {n : ℕ} (i : fin n) (m : ℕ) (h : m ≤ ↑(⇑(fin.add_nat m) i) := _) :
fin.sub_nat m (⇑(fin.add_nat m) i) h = i
source
@[simp]
theorem fin.nat_add_sub_nat_cast {n m : ℕ} {i : fin (n + m)} (h : n ≤ ↑i) :
⇑(fin.nat_add n) (fin.sub_nat n (⇑(fin.cast _) i) h) = i
source
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
source
@[simp]
theorem fin.coe_div_nat {n m : ℕ} (i : fin (m * n)) :
↑(i.div_nat) = ↑i / n
source
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
source
@[simp]
theorem fin.coe_mod_nat {n m : ℕ} (i : fin (m * n)) :
↑(i.mod_nat) = ↑i % n

recursion and induction principles #

source
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
source
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
source
@[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
source
@[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)
source
def fin.induction {n : ℕ} {C : fin (n + 1) → Sort u_1} (h0 : C 0) (hs : Π (i : fin n), C (⇑fin.cast_succ i) → 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
  • fin.induction h0 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)
source
@[simp]
theorem fin.induction_zero {n : ℕ} {C : fin (n + 1) → Sort u_1} (h0 : C 0) (hs : Π (i : fin n), C (⇑fin.cast_succ i) → C i.succ) :
fin.induction h0 hs 0 = h0
source
@[simp]
theorem fin.induction_succ {n : ℕ} {C : fin (n + 1) → Sort u_1} (h0 : C 0) (hs : Π (i : fin n), C (⇑fin.cast_succ i) → C i.succ) (i : fin n) :
fin.induction h0 hs i.succ = hs i (fin.induction h0 hs (⇑fin.cast_succ i))
source
def fin.induction_on {n : ℕ} (i : fin (n + 1)) {C : fin (n + 1) → Sort u_1} (h0 : C 0) (hs : Π (i : fin n), C (⇑fin.cast_succ i) → 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
source
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
source
@[simp]
theorem fin.cases_zero {n : ℕ} {C : fin n.succ → Sort u_1} {H0 : C 0} {Hs : Π (i : fin n), C i.succ} :
fin.cases H0 Hs 0 = H0
source
@[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) :
fin.cases H0 Hs i.succ = Hs i
source
@[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) :
fin.cases H0 Hs ⟨i.succ, h⟩ = Hs ⟨i, _⟩
source
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
source
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
source
theorem fin.forall_fin_one {p : fin 1 → Prop} :
(∀ (i : fin 1), p i) ↔ p 0
source
theorem fin.exists_fin_one {p : fin 1 → Prop} :
(∃ (i : fin 1), p i) ↔ p 0
source
theorem fin.forall_fin_two {p : fin 2 → Prop} :
(∀ (i : fin 2), p i) ↔ p 0 ∧ p 1
source
theorem fin.exists_fin_two {p : fin 2 → Prop} :
(∃ (i : fin 2), p i) ↔ p 0 ∨ p 1
source
theorem fin.fin_two_eq_of_eq_zero_iff {a b : fin 2} (h : a = 0 ↔ b = 0) :
a = b
source
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 (⇑fin.cast_succ 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
source
@[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.cast_succ i)) :
fin.reverse_induction h0 hs (fin.last n) = h0
source
@[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 (⇑fin.cast_succ i)) (i : fin n) :
fin.reverse_induction h0 hs (⇑fin.cast_succ i) = hs i (fin.reverse_induction h0 hs i.succ)
source
def fin.last_cases {n : ℕ} {C : fin (n + 1) → Sort u_1} (hlast : C (fin.last n)) (hcast : Π (i : fin n), C (⇑fin.cast_succ 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.cast_succ, j : fin n.

Equations
source
@[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.cast_succ i)) :
fin.last_cases hlast hcast (fin.last n) = hlast
source
@[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 (⇑fin.cast_succ i)) (i : fin n) :
fin.last_cases hlast hcast (⇑fin.cast_succ i) = hcast i
source
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
source
@[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) :
fin.add_cases hleft hright (⇑(fin.cast_add n) i) = hleft i
source
@[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) :
fin.add_cases hleft hright (⇑(fin.nat_add m) i) = hright i
source
theorem fin.lift_fun_iff_succ {n : ℕ} {α : Type u_1} (r : α → α → Prop) [is_trans α r] {f : fin (n + 1) → α} :
(has_lt.lt ⇒ r) f f ↔ ∀ (i : fin n), r (f (⇑fin.cast_succ i)) (f i.succ)
source
theorem fin.strict_mono_iff_lt_succ {n : ℕ} {α : Type u_1} [preorder α] {f : fin (n + 1) → α} :
strict_mono f ↔ ∀ (i : fin n), f (⇑fin.cast_succ i) < 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.

source
theorem fin.monotone_iff_le_succ {n : ℕ} {α : Type u_1} [preorder α] {f : fin (n + 1) → α} :
monotone f ↔ ∀ (i : fin n), f (⇑fin.cast_succ i) ≤ f i.succ

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

source
theorem fin.strict_anti_iff_succ_lt {n : ℕ} {α : Type u_1} [preorder α] {f : fin (n + 1) → α} :
strict_anti f ↔ ∀ (i : fin n), f i.succ < f (⇑fin.cast_succ i)

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

source
theorem fin.antitone_iff_succ_le {n : ℕ} {α : Type u_1} [preorder α] {f : fin (n + 1) → α} :
antitone f ↔ ∀ (i : fin n), f i.succ ≤ f (⇑fin.cast_succ i)

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

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

Negation on fin n

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

Abelian group structure on fin n.

Equations
source
@[protected, instance]
def fin.has_involutive_neg (n : ℕ) :
has_involutive_neg (fin n)

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

Equations
source
@[protected, instance]
def fin.is_cancel_add (n : ℕ) :
is_cancel_add (fin n)

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

source
@[protected, instance]
def fin.add_left_cancel_semigroup (n : ℕ) :
add_left_cancel_semigroup (fin n)

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

Equations
source
@[protected, instance]
def fin.add_right_cancel_semigroup (n : ℕ) :
add_right_cancel_semigroup (fin n)

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

Equations
source
@[protected]
theorem fin.coe_neg {n : ℕ} (a : fin n) :
↑-a = (n - ↑a) % n
source
@[protected]
theorem fin.coe_sub {n : ℕ} (a b : fin n) :
↑(a - b) = (↑a + (n - ↑b)) % n
source
@[simp]
theorem fin.coe_fin_one (a : fin 1) :
↑a = 0
source
@[simp]
theorem fin.coe_neg_one {n : ℕ} :
↑-1 = n
source
theorem fin.coe_sub_one {n : ℕ} (a : fin (n + 1)) :
↑(a - 1) = ite (a = 0) n (↑a - 1)
source
theorem fin.coe_sub_iff_le {n : ℕ} {a b : fin n} :
↑(a - b) = ↑a - ↑b ↔ b ≤ a
source
theorem fin.coe_sub_iff_lt {n : ℕ} {a b : fin n} :
↑(a - b) = n + ↑a - ↑b ↔ a < b
source
@[simp]
theorem fin.lt_sub_one_iff {n : ℕ} {k : fin (n + 2)} :
k < k - 1 ↔ k = 0
source
@[simp]
theorem fin.le_sub_one_iff {n : ℕ} {k : fin (n + 1)} :
k ≤ k - 1 ↔ k = 0
source
@[simp]
theorem fin.sub_one_lt_iff {n : ℕ} {k : fin (n + 1)} :
k - 1 < k ↔ 0 < k
source
theorem fin.last_sub {n : ℕ} (i : fin (n + 1)) :
fin.last n - i = ⇑fin.rev i
source
theorem fin.succ_above_aux {n : ℕ} (p : fin (n + 1)) :
strict_mono (λ (i : fin n), ite (⇑fin.cast_succ i < p) (⇑fin.cast_succ i) i.succ)
source
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
source
theorem fin.succ_above_below {n : ℕ} (p : fin (n + 1)) (i : fin n) (h : ⇑fin.cast_succ i < p) :
⇑(p.succ_above) i = ⇑fin.cast_succ i

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.

source
@[simp]
theorem fin.succ_above_ne_zero_zero {n : ℕ} [ne_zero n] {a : fin (n + 1)} (ha : a ≠ 0) :
⇑(a.succ_above) 0 = 0
source
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
source
theorem fin.succ_above_ne_zero {n : ℕ} [ne_zero n] {a : fin (n + 1)} {b : fin n} (ha : a ≠ 0) (hb : b ≠ 0) :
⇑(a.succ_above) b ≠ 0
source
@[simp]
theorem fin.succ_above_zero {n : ℕ} :
⇑(0.succ_above) = fin.succ

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

source
@[simp]
theorem fin.succ_above_last {n : ℕ} :
(fin.last n).succ_above = fin.cast_succ

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

source
theorem fin.succ_above_last_apply {n : ℕ} (i : fin n) :
⇑((fin.last n).succ_above) i = ⇑fin.cast_succ i
source
theorem fin.succ_above_above {n : ℕ} (p : fin (n + 1)) (i : fin n) (h : p ≤ ⇑fin.cast_succ i) :
⇑(p.succ_above) 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.

source
theorem fin.succ_above_lt_ge {n : ℕ} (p : fin (n + 1)) (i : fin n) :
⇑fin.cast_succ i < p ∨ p ≤ ⇑fin.cast_succ i

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

source
theorem fin.succ_above_lt_gt {n : ℕ} (p : fin (n + 1)) (i : fin n) :
⇑fin.cast_succ i < p ∨ p < i.succ

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

source
@[simp]
theorem fin.succ_above_lt_iff {n : ℕ} (p : fin (n + 1)) (i : fin n) :
⇑(p.succ_above) i < p ↔ ⇑fin.cast_succ 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.

source
theorem fin.lt_succ_above_iff {n : ℕ} (p : fin (n + 1)) (i : fin n) :
p < ⇑(p.succ_above) i ↔ p ≤ ⇑fin.cast_succ 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.

source
theorem fin.succ_above_ne {n : ℕ} (p : fin (n + 1)) (i : fin n) :
⇑(p.succ_above) i ≠ p

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

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

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

source
@[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
source
@[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
source
theorem fin.cast_lt_succ_above {n : ℕ} {x : fin n} {y : fin (n + 1)} (h : ⇑fin.cast_succ x < y) (h' : (⇑(y.succ_above) x).val < n := _) :
(⇑(y.succ_above) x).cast_lt h' = x
source
theorem fin.pred_succ_above {n : ℕ} {x : fin n} {y : fin (n + 1)} (h : y ≤ ⇑fin.cast_succ x) (h' : ⇑(y.succ_above) x ≠ 0 := _) :
(⇑(y.succ_above) x).pred h' = x
source
theorem fin.exists_succ_above_eq {n : ℕ} {x y : fin (n + 1)} (h : x ≠ y) :
∃ (z : fin n), ⇑(y.succ_above) z = x
source
@[simp]
theorem fin.exists_succ_above_eq_iff {n : ℕ} {x y : fin (n + 1)} :
(∃ (z : fin n), ⇑(x.succ_above) z = y) ↔ y ≠ x
source
@[simp]
theorem fin.range_succ_above {n : ℕ} (p : fin (n + 1)) :
set.range ⇑(p.succ_above) = {p}ᶜ

The range of p.succ_above is everything except p.

source
@[simp]
theorem fin.range_succ (n : ℕ) :
set.range fin.succ = {0}ᶜ
source
@[simp]
theorem fin.exists_succ_eq_iff {n : ℕ} {x : fin (n + 1)} :
(∃ (y : fin n), y.succ = x) ↔ x ≠ 0
source
theorem fin.succ_above_right_injective {n : ℕ} {x : fin (n + 1)} :
function.injective ⇑(x.succ_above)

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

source
theorem fin.succ_above_right_inj {n : ℕ} {a b : fin n} {x : fin (n + 1)} :
⇑(x.succ_above) a = ⇑(x.succ_above) b ↔ a = b

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

source
theorem fin.succ_above_left_injective {n : ℕ} :
function.injective fin.succ_above

succ_above is injective at the pivot

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

succ_above is injective at the pivot

source
@[simp]
theorem fin.zero_succ_above {n : ℕ} (i : fin n) :
⇑(0.succ_above) i = i.succ
source
@[simp]
theorem fin.succ_succ_above_zero {n : ℕ} [ne_zero n] (i : fin n) :
⇑(i.succ.succ_above) 0 = 0
source
@[simp]
theorem fin.succ_succ_above_succ {n : ℕ} (i : fin (n + 1)) (j : fin n) :
⇑(i.succ.succ_above) j.succ = (⇑(i.succ_above) j).succ
source
@[simp]
theorem fin.one_succ_above_zero {n : ℕ} :
⇑(1.succ_above) 0 = 0
source
@[simp]
theorem fin.succ_succ_above_one {n : ℕ} [ne_zero n] (i : fin (n + 1)) :
⇑(i.succ.succ_above) 1 = (⇑(i.succ_above) 0).succ

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

source
@[simp]
theorem fin.one_succ_above_succ {n : ℕ} (j : fin n) :
⇑(1.succ_above) j.succ = j.succ.succ
source
@[simp]
theorem fin.one_succ_above_one {n : ℕ} :
⇑(1.succ_above) 1 = 2
source
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
source
theorem fin.pred_above_right_monotone {n : ℕ} (p : fin n) :
monotone p.pred_above
source
theorem fin.pred_above_left_monotone {n : ℕ} (i : fin (n + 1)) :
monotone (λ (p : fin n), p.pred_above i)
source
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
source
@[simp]
theorem fin.cast_pred_zero {n : ℕ} :
0.cast_pred = 0
source
@[simp]
theorem fin.cast_pred_one {n : ℕ} :
1.cast_pred = 1
source
@[simp]
theorem fin.pred_above_zero {n : ℕ} {i : fin (n + 2)} (hi : i ≠ 0) :
0.pred_above i = i.pred hi
source
@[simp]
theorem fin.cast_pred_last {n : ℕ} :
(fin.last (n + 1)).cast_pred = fin.last n
source
@[simp]
theorem fin.cast_pred_mk (n i : ℕ) (h : i < n + 1) :
⟨i, _⟩.cast_pred = ⟨i, h⟩
source
theorem fin.coe_cast_pred {n : ℕ} (a : fin (n + 2)) (hx : a < fin.last (n + 1)) :
↑(a.cast_pred) = ↑a
source
theorem fin.pred_above_below {n : ℕ} (p : fin (n + 1)) (i : fin (n + 2)) (h : i ≤ ⇑fin.cast_succ p) :
p.pred_above i = i.cast_pred
source
@[simp]
theorem fin.pred_above_last {n : ℕ} :
(fin.last n).pred_above = fin.cast_pred
source
theorem fin.pred_above_last_apply {n : ℕ} (i : fin n) :
(fin.last n).pred_above ↑i = ↑i.cast_pred
source
theorem fin.pred_above_above {n : ℕ} (p : fin n) (i : fin (n + 1)) (h : ⇑fin.cast_succ p < i) :
p.pred_above i = i.pred _
source
theorem fin.cast_pred_monotone {n : ℕ} :
monotone fin.cast_pred
source
@[simp]
theorem fin.succ_above_pred_above {n : ℕ} {p : fin n} {i : fin (n + 1)} (h : i ≠ ⇑fin.cast_succ p) :
⇑((⇑fin.cast_succ p).succ_above) (p.pred_above 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.

source
@[simp]
theorem fin.pred_above_succ_above {n : ℕ} (p i : fin n) :
p.pred_above (⇑((⇑fin.cast_succ p).succ_above) 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.

source
theorem fin.cast_succ_pred_eq_pred_cast_succ {n : ℕ} {a : fin (n + 1)} (ha : a ≠ 0) (ha' : ⇑fin.cast_succ a ≠ 0 := _) :
⇑fin.cast_succ (a.pred ha) = (⇑fin.cast_succ a).pred ha'
source
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.

source
@[simp]
theorem fin.succ_pred_above_succ {n : ℕ} (a : fin n) (b : fin (n + 1)) :
a.succ.pred_above b.succ = (a.pred_above b).succ

succ commutes with pred_above.

source
@[simp]
theorem fin.cast_pred_cast_succ {n : ℕ} (i : fin (n + 1)) :
(⇑fin.cast_succ i).cast_pred = i
source
theorem fin.cast_succ_cast_pred {n : ℕ} {i : fin (n + 2)} (h : i < fin.last (n + 1)) :
⇑fin.cast_succ i.cast_pred = i
source
theorem fin.coe_cast_pred_le_self {n : ℕ} (i : fin (n + 2)) :
↑(i.cast_pred) ≤ ↑i
source
theorem fin.coe_cast_pred_lt_iff {n : ℕ} {i : fin (n + 2)} :
↑(i.cast_pred) < ↑i ↔ i = fin.last (n + 1)
source
theorem fin.lt_last_iff_coe_cast_pred {n : ℕ} {i : fin (n + 2)} :
i < fin.last (n + 1) ↔ ↑(i.cast_pred) = ↑i
source
def fin.clamp (n m : ℕ) :
fin (m + 1)

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

Equations
source
@[simp]
theorem fin.coe_clamp (n m : ℕ) :
↑(fin.clamp n m) = linear_order.min n m
source
@[simp]
theorem fin.coe_of_nat_eq_mod (m n : ℕ) [ne_zero m] :
↑↑n = n % m

mul #

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