ofLinearEquiv — Mathlib

English

Upgrade a linear equivalence to an algebra equivalence provided it preserves multiplication and the unit.

Русский

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

LaTeX

$$$\\text{ofLinearEquiv} : A_1 \\simeq_{R} A_2 $ ( лин Экв )$$

Lean4

/-- Upgrade a linear equivalence to an algebra equivalence,
given that it distributes over multiplication and the identity
-/
@[simps apply]
def ofLinearEquiv : A₁ ≃ₐ[R] A₂ :=
  { l with
    toFun := l
    invFun := l.symm
    map_mul' := map_mul
    commutes' := (AlgHom.ofLinearMap l map_one map_mul : A₁ →ₐ[R] A₂).commutes }

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