toLinearEquiv — Mathlib

English

An isomorphism of algebras becomes a linear isomorphism when the multiplicative structure is forgotten.

Русский

Изоморфизм алгебр превращается в линейное изоморфизм при забывании умножения.

LaTeX

$$$\\mathrm{toLinearEquiv}(e) : A_1 \\to A_2 \\text{ is a linear equivalence with respect to the underlying }R\\text{-module structure}$$$

Lean4

/-- Forgetting the multiplicative structures, an equivalence of algebras is a linear equivalence. -/
@[simps apply]
def toLinearEquiv (e : A₁ ≃ₐ[R] A₂) : A₁ ≃ₗ[R] A₂ :=
  { e with
    toFun := e
    map_smul' := map_smul e
    invFun := e.symm }

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