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