toLinearMap_ofAlgHom — Mathlib

English

A similar statement to 424 holds showing the linear map underlying a constructed AlgEquiv built from f,g matches f's linear map.

Русский

Схожее утверждение показывает соответствие линейного отображения.

LaTeX

$$$\\mathrm{toLinearMap}$ of (\\mathrm{ofAlgHom} f g h_1 h_2) = f$ as linear maps.$$

Lean4

theorem toLinearMap_ofAlgHom (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ h₂) :
    (ofAlgHom f g h₁ h₂).toLinearMap = f.toLinearMap :=
  LinearMap.ext fun _ => rfl

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