toEquiv_symm — Mathlib

English

Let e be a semilinear equivalence between modules. Then the underlying equivalence of its inverse is the inverse of the underlying equivalence.

Русский

Пусть e — полулинейное эквивалентность между модулями. Тогда базовая эквивалентность обратной эквивалентности равна обратной базовой эквивалентности.

LaTeX

$$$\\bigl(\\mathrm{toEquiv}(e)\\bigr)^{-1} = \\mathrm{toEquiv}(e^{-1})$$$

Lean4

@[simp]
theorem toEquiv_symm : e.symm.toEquiv = e.toEquiv.symm :=
  rfl

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