cast_val_eq_self — Mathlib

English

For every a ∈ Fin n, casting its value back to Fin n yields the original element: (a.val : Fin n) = a.

Русский

Для любого a ∈ Fin n приведение его значения обратно к Fin n даёт исходный элемент: (a.val : Fin n) = a.

LaTeX

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

Lean4

/-- If `n` is non-zero, converting the value of a `Fin n` to `Fin n` results
in the same value. -/
@[simp, norm_cast]
theorem cast_val_eq_self {n : ℕ} [NeZero n] (a : Fin n) : (a.val : Fin n) = a :=
  Fin.ext <| val_cast_of_lt a.isLt

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