ofLinearEquiv_symm — Mathlib

English

Upgrading a linear equivalence to an algebra equivalence with the compatible multiplicative structure yields the original linear equivalence.

Русский

Преобразование линейного эквивалентного отображения в алгебраическое эквивалентное отображение с сохранением произведения восстанавливает исходное линейное эквивалентное отображение.

LaTeX

$$$ \\mathrm{ofLinearEquiv} \\; l \\; map\\_mul \\; map\\_one = e $$$

Lean4

@[simp]
theorem ofLinearEquiv_symm :
    (ofLinearEquiv l map_one map_mul).symm =
      ofLinearEquiv l.symm (_root_.map_one <| ofLinearEquiv_symm.aux l map_one map_mul)
        (_root_.map_mul <| ofLinearEquiv_symm.aux l map_one map_mul) :=
  rfl

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