toLinearMap_toAlgHom — Mathlib

English

For any F with AlgHomClass, the underlying linear map associated to toAlgHom f equals f itself as a linear map.

Русский

Для любого F с AlgHomClass соответствующее линейное отображение toAlgHom f совпадает с самим f как линейное отображение.

LaTeX

$$$(AlgHomClass.toAlgHom f : A \\to[R] B) = f$ as linear maps$$

Lean4

@[simp]
theorem _root_.AlgHomClass.toLinearMap_toAlgHom {R A B F : Type*} [CommSemiring R] [Semiring A] [Semiring B]
    [Algebra R A] [Algebra R B] [FunLike F A B] [AlgHomClass F R A B] (f : F) :
    (AlgHomClass.toAlgHom f : A →ₗ[R] B) = f :=
  rfl

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