English
If n = m, then Fin n is canonically equivalent to Fin m via the cast along eq, with inverse given by the cast along eq.symm.
Русский
Если n = m, то Fin n канонически эквивалентно Fin m через приведение по eq, при этом обратное отображение задаётся приведением по eq.symm.
LaTeX
$$$$ \\forall {n,m : \\mathbb{N}} (eq : n = m), \\ Fin\\ n \\cong \\ Fin\\ m. $$$$
Lean4
/-- The 'identity' equivalence between `Fin m` and `Fin n` when `m = n`. -/
@[simps]
def _root_.finCongr (eq : n = m) : Fin n ≃ Fin m
where
toFun := Fin.cast eq
invFun := Fin.cast eq.symm
left_inv := leftInverse_cast eq
right_inv := rightInverse_cast eq
