toLinearEquiv_toLinearMap — Mathlib

English

The linear map underlying the linear equivalence associated to an algebra equivalence is equal to the linear map of the algebra equivalence.

Русский

Линейное отображение, лежащее в основе линейной эквивалентности, совпадает с линейным отображением алгебраической эквивалентности.

LaTeX

$$$e^{\\text{toLinearEquiv}}\\,^{\\;}{\\toLinearMap} = e^{\\text{toLinearMap}}$$$

Lean4

@[simp]
theorem toLinearEquiv_toLinearMap : e.toLinearEquiv.toLinearMap = e.toLinearMap :=
  rfl

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