def Fin.next {n : ℕ} (k : Fin n) : Fin n

Equations

• k.next = ⟨if ↑k + 1 = n then 0 else ↑k + 1, ⋯⟩

theorem Fin.toNat_next_eq {n : ℕ} {k : Fin n} : k.next.toNat = if k.toNat + 1 = n then 0 else k.toNat + 1

@[simp]

theorem Fin.val_eq_val_iff {n : ℕ} {a b : Fin n} : ↑a = ↑b ↔ a = b

def Nat.toFin (k : ℕ) {n : ℕ} [NeZero n] : Fin n

Equations

• k.toFin = Fin.ofNat n k

def Int.toFin (k : ℤ) {n : ℕ} [NeZero n] : Fin n

Equations

• k.toFin = k.toNat.toFin

theorem Nat.toFin_congr {n m : ℕ} [hn : NeZero n] [hm : NeZero m] {k₁ k₂ : ℕ} (h₁ : n = m) (h₂ : k₁ = k₂) : ↑k₁.toFin = ↑k₂.toFin

theorem Int.toFin_congr {n m : ℕ} [hn : NeZero n] [hm : NeZero m] {k₁ k₂ : ℤ} (h₁ : n = m) (h₂ : k₁ = k₂) : ↑k₁.toFin = ↑k₂.toFin

theorem Nat.toFin_eq_self_of {k n : ℕ} [hk : NeZero k] (h : n < k) : ↑n.toFin = n

theorem Int.toFin_eq_self_of {k : ℕ} {z : ℤ} [hk : NeZero k] (h₁ : 0 ≤ z) (h₂ : z < ↑k) : ↑↑z.toFin = z

theorem Int.toFin_eq_toNat_of {k : ℕ} {z : ℤ} [hk : NeZero k] (h₁ : 0 ≤ z) (h₂ : z < ↑k) : ↑z.toFin = z.toNat