ofNat_eq_cast — Mathlib

English

The embedding of natural numbers into Fin(n) via ofNat is the same as the standard cast: Fin.ofNat(n,a) = (a : Fin(n)).

Русский

Встраивание натуральных чисел в Fin(n) через ofNat совпадает с обычным приведением: Fin.ofNat(n,a) = (a : Fin(n)).

LaTeX

$$$$\mathrm{Fin.ofNat}(n,a) = (a:\mathrm{Fin}(n)).$$$$

Lean4

@[simp]
theorem ofNat_eq_cast (n : ℕ) [NeZero n] (a : ℕ) : Fin.ofNat n a = (a : Fin n) :=
  rfl

Похожие утверждения