toLinearEquiv_symm — Mathlib

English

The linear equivalence of the inverse algebra is the inverse of the linear equivalence.

Русский

Линейная эквивалентность обратного алгебраического отображения равна обратной линейной эквивалентности.

LaTeX

$$$\\mathrm{toLinearEquiv}(e^{-1}) = (\\mathrm{toLinearEquiv}(e))^{-1}$$$

Lean4

@[simp]
theorem toLinearEquiv_symm (e : A₁ ≃ₐ[R] A₂) : e.symm.toLinearEquiv = e.toLinearEquiv.symm :=
  rfl

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