toAlgHom_toLinearMap — Mathlib

English

The passage from AlgHom to AlgEquiv preserves the linear map component, i.e., the linear map underlying an equivalence built from AlgHom equals the original linear map.

Русский

Переход от AlgHom к AlgEquiv сохраняет линейную часть отображения.

LaTeX

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

Lean4

@[simp]
theorem toAlgHom_toLinearMap : (e : A₁ →ₐ[R] A₂).toLinearMap = e.toLinearMap :=
  rfl

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