ofLinearEquiv_toLinearEquiv — Mathlib

English

The linear equivalence corresponding to an algebra equivalence is exactly the original linear equivalence used to build it.

Русский

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

LaTeX

$$$ toLinearEquiv(\\mathrm{ofLinearEquiv}(l, map\\_one, map\\_mul)) = l $$$

Lean4

@[simp]
theorem ofLinearEquiv_toLinearEquiv (map_mul) (map_one) : ofLinearEquiv e.toLinearEquiv map_mul map_one = e :=
  rfl

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