The finite type with n elements

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

Main definitions

Induction principles

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

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.succEmb : Fin.succ as an OrderEmbedding;

• Fin.castLEEmb h : Fin.castLE as an OrderEmbedding, embed Fin n into Fin m, h : n ≤ m;

• Fin.castIso : Fin.cast as an OrderIso, order isomorphism between Fin n and Fin m provided that n = m, see also Equiv.finCongr;

• Fin.castAddEmb m : Fin.castAdd as an OrderEmbedding, embed Fin n into Fin (n+m);

• Fin.castSuccEmb : Fin.castSucc as an OrderEmbedding, embed Fin n into Fin (n+1);

• Fin.addNatEmb m i : Fin.addNat as an OrderEmbedding, add m on i on the right, generalizes Fin.succ;

• Fin.natAddEmb n i : Fin.natAdd as an OrderEmbedding, adds n on i on the left;

Other casts

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

Misc definitions

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

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

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

Equations

• finZeroElim x = Fin.elim0 x

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

Equations

• ⋯ = ⋯

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

A dependent variant of Fin.elim0.

Equations

• Fin.rec0 i = absurd ⋯ ⋯

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

theorem Fin.size_positive {n : ℕ} : Fin n → 0 < n

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

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

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

@[simp]

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

@[simp]

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

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

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

Equations

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

coercions and constructions

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

@[deprecated Fin.ext_iff]

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

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

@[simp]

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

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

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

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

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

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

order

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

@[simp]

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

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

@[simp]

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

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

instance Fin.instLinearOrderFin {n : ℕ} : LinearOrder (Fin n)

Equations

• Fin.instLinearOrderFin = LinearOrder.liftWithOrd Fin.val ⋯ ⋯ ⋯ ⋯

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

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

instance Fin.instPartialOrderFin {n : ℕ} : PartialOrder (Fin n)

Equations

• Fin.instPartialOrderFin = inferInstance

theorem Fin.val_strictMono {n : ℕ} : StrictMono Fin.val

@[simp]

theorem Fin.orderIsoSubtype_apply {n : ℕ} (a : Fin n) : Fin.orderIsoSubtype a = { val := ↑a, property := ⋯ }

@[simp]

theorem Fin.orderIsoSubtype_symm_apply {n : ℕ} (a : { i : ℕ // i < n }) : (RelIso.symm Fin.orderIsoSubtype) a = { val := ↑a, isLt := ⋯ }

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

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

Equations

• Fin.orderIsoSubtype = Equiv.toOrderIso Fin.equivSubtype ⋯ ⋯

@[simp]

theorem Fin.valEmbedding_apply {n : ℕ} (self : Fin n) : Fin.valEmbedding self = ↑self

def Fin.valEmbedding {n : ℕ} : Fin n ↪ ℕ

The inclusion map Fin n → ℕ is an embedding.

Equations

• Fin.valEmbedding = { toFun := Fin.val, inj' := ⋯ }

@[simp]

theorem Fin.equivSubtype_symm_trans_valEmbedding {n : ℕ} : Function.Embedding.trans (Equiv.toEmbedding Fin.equivSubtype.symm) Fin.valEmbedding = Function.Embedding.subtype fun (x : ℕ) => x < n

@[simp]

theorem Fin.valOrderEmbedding_apply (n : ℕ) (self : Fin n) : (Fin.valOrderEmbedding n) self = ↑self

def Fin.valOrderEmbedding (n : ℕ) : Fin n ↪o ℕ

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

Equations

• Fin.valOrderEmbedding n = { toEmbedding := Fin.valEmbedding, map_rel_iff' := ⋯ }

instance Fin.Lt.isWellOrder (n : ℕ) : IsWellOrder (Fin n) fun (x x_1 : Fin n) => x < x_1

The ordering on Fin n is a well order.

Equations

• ⋯ = ⋯

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

Use the ordering on Fin n for checking recursive definitions.

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

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

Equations

• Fin.instWellFoundedRelationFin = measure Fin.val

def Fin.ofNat'' {n : ℕ} [NeZero n] (i : ℕ) : Fin n

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

Equations

• Fin.ofNat'' i = { val := i % n, isLt := ⋯ }

instance Fin.instZeroFin {n : ℕ} [NeZero n] : Zero (Fin n)

Equations

• Fin.instZeroFin = { zero := Fin.ofNat'' 0 }

instance Fin.instOneFin {n : ℕ} [NeZero n] : One (Fin n)

Equations

• Fin.instOneFin = { one := Fin.ofNat'' 1 }

@[simp]

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

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

@[simp]

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

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

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

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

@[simp]

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

theorem Fin.rev_involutive {n : ℕ} : Function.Involutive Fin.rev

@[simp]

theorem Fin.revPerm_symm_apply {n : ℕ} (i : Fin n) : Fin.revPerm.symm i = Fin.rev i

@[simp]

theorem Fin.revPerm_apply {n : ℕ} (i : Fin n) : Fin.revPerm i = Fin.rev i

def Fin.revPerm {n : ℕ} : Equiv.Perm (Fin n)

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

Equations

• Fin.revPerm = Function.Involutive.toPerm Fin.rev ⋯

theorem Fin.rev_injective {n : ℕ} : Function.Injective Fin.rev

theorem Fin.rev_surjective {n : ℕ} : Function.Surjective Fin.rev

theorem Fin.rev_bijective {n : ℕ} : Function.Bijective Fin.rev

@[simp]

theorem Fin.revPerm_symm {n : ℕ} : Fin.revPerm.symm = Fin.revPerm

@[simp]

theorem Fin.revOrderIso_apply {n : ℕ} : ∀ (a : (Fin n)ᵒᵈ), Fin.revOrderIso a = Fin.rev (OrderDual.ofDual a)

@[simp]

theorem Fin.revOrderIso_toEquiv {n : ℕ} : Fin.revOrderIso.toEquiv = OrderDual.ofDual.trans Fin.revPerm

def Fin.revOrderIso {n : ℕ} : (Fin n)ᵒᵈ ≃o Fin n

Fin.rev n as an order-reversing isomorphism.

Equations

• Fin.revOrderIso = { toEquiv := OrderDual.ofDual.trans Fin.revPerm, map_rel_iff' := ⋯ }

@[simp]

theorem Fin.revOrderIso_symm_apply {n : ℕ} (i : Fin n) : (OrderIso.symm Fin.revOrderIso) i = OrderDual.toDual (Fin.rev i)

theorem Fin.cast_rev {n : ℕ} {m : ℕ} (i : Fin n) (h : n = m) : Fin.cast h (Fin.rev i) = Fin.rev (Fin.cast h i)

theorem Fin.rev_eq_iff {n : ℕ} {i : Fin n} {j : Fin n} : Fin.rev i = j ↔ i = Fin.rev j

theorem Fin.rev_ne_iff {n : ℕ} {i : Fin n} {j : Fin n} : Fin.rev i ≠ j ↔ i ≠ Fin.rev j

theorem Fin.rev_lt_iff {n : ℕ} {i : Fin n} {j : Fin n} : Fin.rev i < j ↔ Fin.rev j < i

theorem Fin.rev_le_iff {n : ℕ} {i : Fin n} {j : Fin n} : Fin.rev i ≤ j ↔ Fin.rev j ≤ i

theorem Fin.lt_rev_iff {n : ℕ} {i : Fin n} {j : Fin n} : i < Fin.rev j ↔ j < Fin.rev i

theorem Fin.le_rev_iff {n : ℕ} {i : Fin n} {j : Fin n} : i ≤ Fin.rev j ↔ j ≤ Fin.rev i

instance Fin.instBoundedOrderFinHAddNatInstHAddInstAddNatOfNatInstLEFin {n : ℕ} : BoundedOrder (Fin (n + 1))

Equations

• Fin.instBoundedOrderFinHAddNatInstHAddInstAddNatOfNatInstLEFin = BoundedOrder.mk

instance Fin.instLatticeFinHAddNatInstHAddInstAddNatOfNat {n : ℕ} : Lattice (Fin (n + 1))

Equations

• Fin.instLatticeFinHAddNatInstHAddInstAddNatOfNat = LinearOrder.toLattice

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

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

theorem Fin.top_eq_last (n : ℕ) : ⊤ = Fin.last n

theorem Fin.bot_eq_zero (n : ℕ) : ⊥ = 0

@[simp]

theorem Fin.coe_orderIso_apply {n : ℕ} {m : ℕ} (e : Fin n ≃o Fin m) (i : Fin n) : ↑(e 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} [Preorder α] : Subsingleton (Fin n ≃o α)

Equations

• ⋯ = ⋯

instance Fin.orderIso_subsingleton' {n : ℕ} {α : Type u_1} [Preorder α] : Subsingleton (α ≃o Fin n)

Equations

• ⋯ = ⋯

instance Fin.orderIsoUnique {n : ℕ} : Unique (Fin n ≃o Fin n)

Equations

• Fin.orderIsoUnique = Unique.mk' (Fin n ≃o Fin n)

theorem Fin.strictMono_unique {n : ℕ} {α : Type u_1} [Preorder α] {f : Fin n → α} {g : Fin n → α} (hf : StrictMono f) (hg : StrictMono 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.

theorem Fin.orderEmbedding_eq {n : ℕ} {α : Type u_1} [Preorder α] {f : Fin n ↪o α} {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

@[simp]

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

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

instance Fin.nontrivial {n : ℕ} : Nontrivial (Fin (n + 2))

Equations

• ⋯ = ⋯

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

instance Fin.addCommSemigroup (n : ℕ) : AddCommSemigroup (Fin n)

Equations

• Fin.addCommSemigroup n = AddCommSemigroup.mk ⋯

theorem Fin.add_zero {n : ℕ} [NeZero n] (k : Fin n) : k + 0 = k

theorem Fin.zero_add {n : ℕ} [NeZero n] (k : Fin n) : 0 + k = k

instance Fin.instOfNatFin {n : ℕ} {a : ℕ} [NeZero n] : OfNat (Fin n) a

Equations

• Fin.instOfNatFin = { ofNat := Fin.ofNat' a ⋯ }

instance Fin.inhabited (n : ℕ) [NeZero n] : Inhabited (Fin n)

Equations

• Fin.inhabited n = { default := 0 }

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

Equations

• Fin.inhabitedFinOneAdd n = inferInstance

@[simp]

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

@[simp]

theorem Fin.ofNat'_zero {n : ℕ} {h : n > 0} [NeZero n] : Fin.ofNat' 0 h = 0

@[simp]

theorem Fin.ofNat'_one {n : ℕ} {h : n > 0} [NeZero n] : Fin.ofNat' 1 h = 1

instance Fin.instAddCommSemigroupFin (n : ℕ) : AddCommSemigroup (Fin n)

Equations

• Fin.instAddCommSemigroupFin n = AddCommSemigroup.mk ⋯

instance Fin.addCommMonoid (n : ℕ) [NeZero n] : AddCommMonoid (Fin n)

Equations

• Fin.addCommMonoid n = let __spread.0 := Fin.addCommSemigroup n; AddCommMonoid.mk ⋯

instance Fin.instAddMonoidWithOne (n : ℕ) [NeZero n] : AddMonoidWithOne (Fin n)

Equations

• Fin.instAddMonoidWithOne n = let __spread.0 := inferInstanceAs (AddCommMonoid (Fin n)); AddMonoidWithOne.mk ⋯ ⋯

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

@[deprecated]

theorem Fin.val_bit0 {n : ℕ} (k : Fin n) : ↑(bit0 k) = bit0 ↑k % n

@[deprecated]

theorem Fin.val_bit1 {n : ℕ} [NeZero n] (k : Fin n) : ↑(bit1 k) = bit1 ↑k % n

@[simp, deprecated]

theorem Fin.mk_bit0 {m : ℕ} {n : ℕ} (h : bit0 m < n) : { val := bit0 m, isLt := h } = bit0 { val := m, isLt := ⋯ }

@[simp, deprecated]

theorem Fin.mk_bit1 {m : ℕ} {n : ℕ} [NeZero n] (h : bit1 m < n) : { val := bit1 m, isLt := h } = bit1 { val := m, isLt := ⋯ }

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem Fin.one_eq_zero_iff {n : ℕ} [NeZero n] : 1 = 0 ↔ n = 1

@[simp]

theorem Fin.zero_eq_one_iff {n : ℕ} [NeZero n] : 0 = 1 ↔ n = 1

succ and casts into larger Fin types

theorem Fin.strictMono_succ {n : ℕ} : StrictMono Fin.succ

def Fin.succEmb (n : ℕ) : Fin n ↪o Fin (n + 1)

Fin.succ as an OrderEmbedding

Equations

• Fin.succEmb n = OrderEmbedding.ofStrictMono Fin.succ ⋯

@[simp]

theorem Fin.val_succEmb {n : ℕ} : ⇑(Fin.succEmb n) = Fin.succ

@[simp]

theorem Fin.exists_succ_eq {n : ℕ} {x : Fin (n + 1)} : (∃ (y : Fin n), Fin.succ y = x) ↔ x ≠ 0

theorem Fin.exists_succ_eq_of_ne_zero {n : ℕ} {x : Fin (n + 1)} (h : x ≠ 0) : ∃ (y : Fin n), Fin.succ y = x

theorem Fin.succ_injective (n : ℕ) : Function.Injective Fin.succ

@[simp]

theorem Fin.succ_zero_eq_one' {n : ℕ} [NeZero n] : Fin.succ 0 = 1

theorem Fin.one_pos' {n : ℕ} [NeZero n] : 0 < 1

theorem Fin.zero_ne_one' {n : ℕ} [NeZero n] : 0 ≠ 1

@[simp]

theorem Fin.succ_one_eq_two' {n : ℕ} [NeZero n] : Fin.succ 1 = 2

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

@[simp]

theorem Fin.le_zero_iff' {n : ℕ} [NeZero n] {k : Fin n} : k ≤ 0 ↔ k = 0

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

@[simp]

theorem Fin.cast_refl {n : ℕ} (h : n = n) : Fin.cast h = id

theorem Fin.strictMono_castLE {n : ℕ} {m : ℕ} (h : n ≤ m) : StrictMono (Fin.castLE h)

theorem Fin.castLE_injective {n : ℕ} {m : ℕ} (hmn : m ≤ n) : Function.Injective (Fin.castLE hmn)

@[simp]

theorem Fin.castLE_inj {n : ℕ} {m : ℕ} {hmn : m ≤ n} {a : Fin m} {b : Fin m} : Fin.castLE hmn a = Fin.castLE hmn b ↔ a = b

@[simp]

theorem Fin.castLEEmb_toEmbedding {n : ℕ} {m : ℕ} (h : n ≤ m) : (Fin.castLEEmb h).toEmbedding = { toFun := Fin.castLE h, inj' := ⋯ }

@[simp]

theorem Fin.castLEEmb_apply {n : ℕ} {m : ℕ} (h : n ≤ m) (i : Fin n) : (Fin.castLEEmb h) i = Fin.castLE h i

def Fin.castLEEmb {n : ℕ} {m : ℕ} (h : n ≤ m) : Fin n ↪o Fin m

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

Equations

• Fin.castLEEmb h = OrderEmbedding.ofStrictMono (Fin.castLE h) ⋯

theorem Fin.nonempty_embedding_iff {n : ℕ} {m : ℕ} : Nonempty (Fin n ↪ Fin m) ↔ n ≤ m

theorem Fin.equiv_iff_eq {n : ℕ} {m : ℕ} : Nonempty (Fin m ≃ Fin n) ↔ m = n

@[simp]

theorem Fin.castLE_castSucc {n : ℕ} {m : ℕ} (i : Fin n) (h : n + 1 ≤ m) : Fin.castLE h (Fin.castSucc i) = Fin.castLE ⋯ i

@[simp]

theorem Fin.castLE_comp_castSucc {n : ℕ} {m : ℕ} (h : n + 1 ≤ m) : Fin.castLE h ∘ Fin.castSucc = Fin.castLE ⋯

@[simp]

theorem Fin.castLE_rfl (n : ℕ) : Fin.castLE ⋯ = id

@[simp]

theorem Fin.range_castLE {n : ℕ} {k : ℕ} (h : n ≤ k) : Set.range (Fin.castLE h) = {i : Fin k | ↑i < n}

@[simp]

theorem Fin.coe_of_injective_castLEEmb_symm {n : ℕ} {k : ℕ} (h : n ≤ k) (i : Fin k) (hi : i ∈ Set.range ⇑(Fin.castLEEmb h)) : ↑((Equiv.ofInjective ⇑(Fin.castLEEmb h) ⋯).symm { val := i, property := hi }) = ↑i

theorem Fin.leftInverse_cast {n : ℕ} {m : ℕ} (eq : n = m) : Function.LeftInverse (Fin.cast ⋯) (Fin.cast eq)

theorem Fin.rightInverse_cast {n : ℕ} {m : ℕ} (eq : n = m) : Function.RightInverse (Fin.cast ⋯) (Fin.cast eq)

theorem Fin.cast_le_cast {n : ℕ} {m : ℕ} (eq : n = m) {a : Fin n} {b : Fin n} : Fin.cast eq a ≤ Fin.cast eq b ↔ a ≤ b

@[simp]

theorem Fin.castIso_apply {n : ℕ} {m : ℕ} (eq : n = m) (i : Fin n) : (Fin.castIso eq) i = Fin.cast eq i

@[simp]

theorem Fin.castIso_symm_apply {n : ℕ} {m : ℕ} (eq : n = m) (i : Fin m) : (RelIso.symm (Fin.castIso eq)) i = Fin.cast ⋯ i

def Fin.castIso {n : ℕ} {m : ℕ} (eq : n = m) : Fin n ≃o Fin m

Fin.cast as an OrderIso, castIso eq i embeds i into an equal Fin type, see also Equiv.finCongr.

Equations

• Fin.castIso eq = { toEquiv := { toFun := Fin.cast eq, invFun := Fin.cast ⋯, left_inv := ⋯, right_inv := ⋯ }, map_rel_iff' := ⋯ }

@[simp]

theorem Fin.symm_castIso {n : ℕ} {m : ℕ} (h : n = m) : OrderIso.symm (Fin.castIso h) = Fin.castIso ⋯

@[simp]

theorem Fin.cast_zero {n : ℕ} {n' : ℕ} [NeZero n] {h : n = n'} : Fin.cast h 0 = 0

@[simp]

theorem Fin.castIso_refl {n : ℕ} (h : optParam (n = n) ⋯) : Fin.castIso h = OrderIso.refl (Fin n)

theorem Fin.castIso_to_equiv {n : ℕ} {m : ℕ} (h : n = m) : (Fin.castIso h).toEquiv = Equiv.cast ⋯

While in many cases Fin.castIso 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) : 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.

theorem Fin.strictMono_castAdd {n : ℕ} (m : ℕ) : StrictMono (Fin.castAdd m)

@[simp]

theorem Fin.castAddEmb_apply {n : ℕ} (m : ℕ) : ∀ (a : Fin n), (Fin.castAddEmb m) a = Fin.castAdd m a

@[simp]

theorem Fin.castAddEmb_toEmbedding {n : ℕ} (m : ℕ) : (Fin.castAddEmb m).toEmbedding = { toFun := Fin.castAdd m, inj' := ⋯ }

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

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

Equations

• Fin.castAddEmb m = OrderEmbedding.ofStrictMono (Fin.castAdd m) ⋯

theorem Fin.strictMono_castSucc {n : ℕ} : StrictMono Fin.castSucc

@[simp]

theorem Fin.castSuccEmb_apply {n : ℕ} : ∀ (a : Fin n), Fin.castSuccEmb a = Fin.castSucc a

@[simp]

theorem Fin.castSuccEmb_toEmbedding {n : ℕ} : Fin.castSuccEmb.toEmbedding = { toFun := Fin.castSucc, inj' := ⋯ }

def Fin.castSuccEmb {n : ℕ} : Fin n ↪o Fin (n + 1)

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

Equations

• Fin.castSuccEmb = OrderEmbedding.ofStrictMono Fin.castSucc ⋯

@[simp]

theorem Fin.castSucc_le_castSucc_iff : ∀ {n : ℕ} {a b : Fin n}, Fin.castSucc a ≤ Fin.castSucc b ↔ a ≤ b

@[simp]

theorem Fin.succ_le_castSucc_iff : ∀ {n : ℕ} {a b : Fin n}, Fin.succ a ≤ Fin.castSucc b ↔ a < b

@[simp]

theorem Fin.castSucc_lt_succ_iff : ∀ {n : ℕ} {a b : Fin n}, Fin.castSucc a < Fin.succ b ↔ a ≤ b

theorem Fin.le_of_castSucc_lt_of_succ_lt {n : ℕ} {a : Fin (n + 1)} {b : Fin (n + 1)} {i : Fin n} (hl : Fin.castSucc i < a) (hu : b < Fin.succ i) : b < a

theorem Fin.castSucc_lt_or_lt_succ {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : Fin.castSucc i < p ∨ p < Fin.succ i

theorem Fin.succ_le_or_le_castSucc {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : Fin.succ i ≤ p ∨ p ≤ Fin.castSucc i

theorem Fin.exists_castSucc_eq_of_ne_last {n : ℕ} {x : Fin (n + 1)} (h : x ≠ Fin.last n) : ∃ (y : Fin n), Fin.castSucc y = x

theorem Fin.castSucc_injective (n : ℕ) : Function.Injective Fin.castSucc

theorem Fin.forall_fin_succ' {n : ℕ} {P : Fin (n + 1) → Prop} : (∀ (i : Fin (n + 1)), P i) ↔ (∀ (i : Fin n), P (Fin.castSucc i)) ∧ P (Fin.last n)

theorem Fin.eq_castSucc_or_eq_last {n : ℕ} (i : Fin (n + 1)) : (∃ (j : Fin n), i = Fin.castSucc j) ∨ i = Fin.last n

theorem Fin.exists_fin_succ' {n : ℕ} {P : Fin (n + 1) → Prop} : (∃ (i : Fin (n + 1)), P i) ↔ (∃ (i : Fin n), P (Fin.castSucc i)) ∨ P (Fin.last n)

@[simp]

theorem Fin.castSucc_zero' {n : ℕ} [NeZero n] : Fin.castSucc 0 = 0

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

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

castSucc i is positive when i is positive.

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

@[simp]

theorem Fin.castSucc_eq_zero_iff' {n : ℕ} [NeZero n] (a : Fin n) : Fin.castSucc a = 0 ↔ a = 0

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

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

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

theorem Fin.castSucc_ne_zero_of_lt {n : ℕ} {p : Fin n} {i : Fin n} (h : p < i) : Fin.castSucc i ≠ 0

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

theorem Fin.succ_ne_last_of_lt {n : ℕ} {p : Fin n} {i : Fin n} (h : i < p) : Fin.succ i ≠ Fin.last n

@[simp]

theorem Fin.coe_eq_castSucc {n : ℕ} {a : Fin n} : ↑↑a = Fin.castSucc a

theorem Fin.coe_succ_lt_iff_lt {n : ℕ} {j : Fin n} {k : Fin n} : ↑↑j < ↑↑k ↔ j < k

@[simp]

theorem Fin.range_castSucc {n : ℕ} : Set.range Fin.castSucc = {i : Fin (Nat.succ n) | ↑i < n}

@[simp]

theorem Fin.coe_of_injective_castSucc_symm {n : ℕ} (i : Fin (Nat.succ n)) (hi : i ∈ Set.range Fin.castSucc) : ↑((Equiv.ofInjective Fin.castSucc ⋯).symm { val := i, property := hi }) = ↑i

theorem Fin.strictMono_addNat {n : ℕ} (m : ℕ) : StrictMono fun (x : Fin n) => Fin.addNat x m

@[simp]

theorem Fin.addNatEmb_toEmbedding {n : ℕ} (m : ℕ) : (Fin.addNatEmb m).toEmbedding = { toFun := fun (x : Fin n) => Fin.addNat x m, inj' := ⋯ }

@[simp]

theorem Fin.addNatEmb_apply {n : ℕ} (m : ℕ) : ∀ (x : Fin n), (Fin.addNatEmb m) x = Fin.addNat x m

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

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

Equations

• Fin.addNatEmb m = OrderEmbedding.ofStrictMono (fun (x : Fin n) => Fin.addNat x m) ⋯

theorem Fin.strictMono_natAdd (n : ℕ) {m : ℕ} : StrictMono (Fin.natAdd n)

@[simp]

theorem Fin.natAddEmb_apply (n : ℕ) {m : ℕ} (i : Fin m) : (Fin.natAddEmb n) i = Fin.natAdd n i

@[simp]

theorem Fin.natAddEmb_toEmbedding (n : ℕ) {m : ℕ} : (Fin.natAddEmb n).toEmbedding = { toFun := Fin.natAdd n, inj' := ⋯ }

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

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

Equations

• Fin.natAddEmb n = OrderEmbedding.ofStrictMono (Fin.natAdd n) ⋯

pred

theorem Fin.strictMono_pred_comp {n : ℕ} {α : Type u_1} [Preorder α] {f : α → Fin (n + 1)} (hf : ∀ (a : α), f a ≠ 0) (hf₂ : StrictMono f) : StrictMono fun (a : α) => Fin.pred (f a) ⋯

theorem Fin.monotone_pred_comp {n : ℕ} {α : Type u_1} [Preorder α] {f : α → Fin (n + 1)} (hf : ∀ (a : α), f a ≠ 0) (hf₂ : Monotone f) : Monotone fun (a : α) => Fin.pred (f a) ⋯

theorem Fin.pred_one' {n : ℕ} [NeZero n] (h : optParam (1 ≠ 0) ⋯) : Fin.pred 1 h = 0

theorem Fin.pred_last {n : ℕ} (h : optParam (Fin.last (n + 1) ≠ 0) ⋯) : Fin.pred (Fin.last (n + 1)) h = Fin.last n

theorem Fin.pred_lt_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) : Fin.pred i hi < j ↔ i < Fin.succ j

theorem Fin.lt_pred_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) : j < Fin.pred i hi ↔ Fin.succ j < i

theorem Fin.pred_le_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) : Fin.pred i hi ≤ j ↔ i ≤ Fin.succ j

theorem Fin.le_pred_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) : j ≤ Fin.pred i hi ↔ Fin.succ j ≤ i

theorem Fin.castSucc_pred_eq_pred_castSucc {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ 0) (ha' : optParam (Fin.castSucc a ≠ 0) ⋯) : Fin.castSucc (Fin.pred a ha) = Fin.pred (Fin.castSucc a) ha'

theorem Fin.castSucc_pred_add_one_eq {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ 0) : Fin.castSucc (Fin.pred a ha) + 1 = a

theorem Fin.le_pred_castSucc_iff {n : ℕ} {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : Fin.castSucc a ≠ 0) : b ≤ Fin.pred (Fin.castSucc a) ha ↔ b < a

theorem Fin.pred_castSucc_lt_iff {n : ℕ} {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : Fin.castSucc a ≠ 0) : Fin.pred (Fin.castSucc a) ha < b ↔ a ≤ b

theorem Fin.pred_castSucc_lt {n : ℕ} {a : Fin (n + 1)} (ha : Fin.castSucc a ≠ 0) : Fin.pred (Fin.castSucc a) ha < a

theorem Fin.le_castSucc_pred_iff {n : ℕ} {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a ≠ 0) : b ≤ Fin.castSucc (Fin.pred a ha) ↔ b < a

theorem Fin.castSucc_pred_lt_iff {n : ℕ} {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a ≠ 0) : Fin.castSucc (Fin.pred a ha) < b ↔ a ≤ b

theorem Fin.castSucc_pred_lt {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ 0) : Fin.castSucc (Fin.pred a ha) < a

@[inline]

def Fin.castPred {n : ℕ} (i : Fin (n + 1)) (h : i ≠ Fin.last n) : Fin n

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

Equations

• Fin.castPred i h = Fin.castLT i ⋯

@[simp]

theorem Fin.castLT_eq_castPred {n : ℕ} (i : Fin (n + 1)) (h : i < Fin.last n) (h' : optParam (i ≠ Fin.last n) ⋯) : Fin.castLT i h = Fin.castPred i h'

@[simp]

theorem Fin.coe_castPred {n : ℕ} (i : Fin (n + 1)) (h : i ≠ Fin.last n) : ↑(Fin.castPred i h) = ↑i

@[simp]

theorem Fin.castPred_castSucc {n : ℕ} {i : Fin n} (h' : optParam (Fin.castSucc i ≠ Fin.last n) ⋯) : Fin.castPred (Fin.castSucc i) h' = i

@[simp]

theorem Fin.castSucc_castPred {n : ℕ} (i : Fin (n + 1)) (h : i ≠ Fin.last n) : Fin.castSucc (Fin.castPred i h) = i

theorem Fin.castPred_eq_iff_eq_castSucc {n : ℕ} (i : Fin (n + 1)) (hi : i ≠ Fin.last n) (j : Fin n) : Fin.castPred i hi = j ↔ i = Fin.castSucc j

@[simp]

theorem Fin.castPred_mk {n : ℕ} (i : ℕ) (h₁ : i < n) (h₂ : optParam (i < Nat.succ n) ⋯) (h₃ : optParam ({ val := i, isLt := h₂ } ≠ Fin.last n) ⋯) : Fin.castPred { val := i, isLt := h₂ } h₃ = { val := i, isLt := h₁ }

theorem Fin.castPred_le_castPred_iff {n : ℕ} {i : Fin (n + 1)} {j : Fin (n + 1)} {hi : i ≠ Fin.last n} {hj : j ≠ Fin.last n} : Fin.castPred i hi ≤ Fin.castPred j hj ↔ i ≤ j

theorem Fin.castPred_lt_castPred_iff {n : ℕ} {i : Fin (n + 1)} {j : Fin (n + 1)} {hi : i ≠ Fin.last n} {hj : j ≠ Fin.last n} : Fin.castPred i hi < Fin.castPred j hj ↔ i < j

theorem Fin.strictMono_castPred_comp {n : ℕ} {α : Type u_1} [Preorder α] {f : α → Fin (n + 1)} (hf : ∀ (a : α), f a ≠ Fin.last n) (hf₂ : StrictMono f) : StrictMono fun (a : α) => Fin.castPred (f a) ⋯

theorem Fin.monotone_castPred_comp {n : ℕ} {α : Type u_1} [Preorder α] {f : α → Fin (n + 1)} (hf : ∀ (a : α), f a ≠ Fin.last n) (hf₂ : Monotone f) : Monotone fun (a : α) => Fin.castPred (f a) ⋯

theorem Fin.castPred_lt_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ Fin.last n) : Fin.castPred i hi < j ↔ i < Fin.castSucc j

theorem Fin.lt_castPred_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ Fin.last n) : j < Fin.castPred i hi ↔ Fin.castSucc j < i

theorem Fin.castPred_le_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ Fin.last n) : Fin.castPred i hi ≤ j ↔ i ≤ Fin.castSucc j

theorem Fin.le_castPred_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ Fin.last n) : j ≤ Fin.castPred i hi ↔ Fin.castSucc j ≤ i

theorem Fin.castPred_inj {n : ℕ} {i : Fin (n + 1)} {j : Fin (n + 1)} {hi : i ≠ Fin.last n} {hj : j ≠ Fin.last n} : Fin.castPred i hi = Fin.castPred j hj ↔ i = j

theorem Fin.castPred_zero' {n : ℕ} [NeZero n] (h : optParam (0 ≠ Fin.last n) ⋯) : Fin.castPred 0 h = 0

theorem Fin.castPred_zero {n : ℕ} (h : optParam (0 ≠ Fin.last (n + 1)) ⋯) : Fin.castPred 0 h = 0

@[simp]

theorem Fin.castPred_one {n : ℕ} [NeZero n] (h : optParam (1 ≠ Fin.last (n + 1)) ⋯) : Fin.castPred 1 h = 1

theorem Fin.rev_pred : ∀ {a : ℕ} {i : Fin (a + 1)} (h : i ≠ 0) (h' : optParam (Fin.rev i ≠ Fin.last a) ⋯), Fin.rev (Fin.pred i h) = Fin.castPred (Fin.rev i) h'

theorem Fin.rev_castPred {n : ℕ} {i : Fin (n + 1)} (h : i ≠ Fin.last n) (h' : optParam (Fin.rev i ≠ 0) ⋯) : Fin.rev (Fin.castPred i h) = Fin.pred (Fin.rev i) h'

theorem Fin.succ_castPred_eq_castPred_succ {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ Fin.last n) (ha' : optParam (Fin.succ a ≠ Fin.last (n + 1)) ⋯) : Fin.succ (Fin.castPred a ha) = Fin.castPred (Fin.succ a) ha'

theorem Fin.succ_castPred_eq_add_one {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ Fin.last n) : Fin.succ (Fin.castPred a ha) = a + 1

theorem Fin.castpred_succ_le_iff {n : ℕ} {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : Fin.succ a ≠ Fin.last (n + 1)) : Fin.castPred (Fin.succ a) ha ≤ b ↔ a < b

theorem Fin.lt_castPred_succ_iff {n : ℕ} {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : Fin.succ a ≠ Fin.last (n + 1)) : b < Fin.castPred (Fin.succ a) ha ↔ b ≤ a

theorem Fin.lt_castPred_succ {n : ℕ} {a : Fin (n + 1)} (ha : Fin.succ a ≠ Fin.last (n + 1)) : a < Fin.castPred (Fin.succ a) ha

theorem Fin.succ_castPred_le_iff {n : ℕ} {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a ≠ Fin.last n) : Fin.succ (Fin.castPred a ha) ≤ b ↔ a < b

theorem Fin.lt_succ_castPred_iff {n : ℕ} {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a ≠ Fin.last n) : b < Fin.succ (Fin.castPred a ha) ↔ b ≤ a

theorem Fin.lt_succ_castPred {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ Fin.last n) : a < Fin.succ (Fin.castPred a ha)

theorem Fin.castPred_le_pred_iff {n : ℕ} {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a ≠ Fin.last n) (hb : b ≠ 0) : Fin.castPred a ha ≤ Fin.pred b hb ↔ a < b

theorem Fin.pred_lt_castPred_iff {n : ℕ} {a : Fin (n + 1)} {b : Fin (n + 1)} (ha : a ≠ 0) (hb : b ≠ Fin.last n) : Fin.pred a ha < Fin.castPred b hb ↔ a ≤ b

theorem Fin.pred_lt_castPred {n : ℕ} {a : Fin (n + 1)} (h₁ : a ≠ 0) (h₂ : a ≠ Fin.last n) : Fin.pred a h₁ < Fin.castPred a h₂

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

• Fin.divNat i = { val := ↑i / n, isLt := ⋯ }

@[simp]

theorem Fin.coe_divNat {n : ℕ} {m : ℕ} (i : Fin (m * n)) : ↑(Fin.divNat i) = ↑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

• Fin.modNat i = { val := ↑i % n, isLt := ⋯ }

@[simp]

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

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

recursion and induction principles

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

theorem Fin.strictMono_iff_lt_succ {n : ℕ} {α : Type u_1} [Preorder α] {f : Fin (n + 1) → α} : StrictMono f ↔ ∀ (i : Fin n), f (Fin.castSucc i) < f (Fin.succ i)

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) → α} : Monotone f ↔ ∀ (i : Fin n), f (Fin.castSucc i) ≤ f (Fin.succ i)

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} [Preorder α] {f : Fin (n + 1) → α} : StrictAnti f ↔ ∀ (i : Fin n), f (Fin.succ i) < f (Fin.castSucc 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} [Preorder α] {f : Fin (n + 1) → α} : Antitone f ↔ ∀ (i : Fin n), f (Fin.succ i) ≤ f (Fin.castSucc 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

• Fin.neg n = { neg := fun (a : Fin n) => { val := (n - ↑a) % n, isLt := ⋯ } }

instance Fin.addCommGroup (n : ℕ) [NeZero n] : AddCommGroup (Fin n)

Abelian group structure on Fin n.

Equations

• Fin.addCommGroup n = let __src := Fin.addCommMonoid n; let __src_1 := Fin.neg n; AddCommGroup.mk ⋯

instance Fin.instInvolutiveNeg (n : ℕ) : InvolutiveNeg (Fin n)

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

Equations

• Fin.instInvolutiveNeg n = InvolutiveNeg.mk ⋯

instance Fin.instIsCancelAdd (n : ℕ) : IsCancelAdd (Fin n)

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

Equations

• ⋯ = ⋯

instance Fin.instAddLeftCancelSemigroup (n : ℕ) : AddLeftCancelSemigroup (Fin n)

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

Equations

• Fin.instAddLeftCancelSemigroup n = let __src := Fin.addCommSemigroup n; let __src_1 := ⋯; AddLeftCancelSemigroup.mk ⋯

instance Fin.instAddRightCancelSemigroup (n : ℕ) : AddRightCancelSemigroup (Fin n)

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

Equations

• Fin.instAddRightCancelSemigroup n = let __src := Fin.addCommSemigroup n; let __src_1 := ⋯; AddRightCancelSemigroup.mk ⋯

theorem Fin.coe_neg {n : ℕ} (a : Fin n) : ↑(-a) = (n - ↑a) % n

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

instance Fin.uniqueFinOne : Unique (Fin 1)

Equations

• Fin.uniqueFinOne = { toInhabited := Fin.inhabited 1, uniq := Fin.uniqueFinOne.proof_2 }

@[simp]

theorem Fin.coe_fin_one (a : Fin 1) : ↑a = 0

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

@[simp]

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

theorem Fin.coe_sub_one {n : ℕ} (a : Fin (n + 1)) : ↑(a - 1) = if a = 0 then n else ↑a - 1

@[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)) : Fin.last n - i = Fin.rev i

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

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

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

@[simp]

theorem Fin.neg_last (n : ℕ) : -Fin.last n = 1

theorem Fin.neg_nat_cast_eq_one (n : ℕ) : -↑n = 1

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

@[simp]

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

mul

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

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

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

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

instance Fin.toExpr (n : ℕ) : Lean.ToExpr (Fin n)

Equations

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