linearMapMk_toAddHom — Mathlib

English

The linear map constructed from an AlgHom via LinearMap.mk with its map_smul data equals the underlying linear map of the AlgHom.

Русский

Линейное отображение, построенное из AlgHom через LinearMap.mk с данными map_smul, равно его toLinearMap.

LaTeX

$$$$\text{LinearMap.mk } f (\mathrm{map\_smul} f) = f^{\mathrm{toLinearMap}}.$$$$

Lean4

@[simp]
theorem linearMapMk_toAddHom (f : A →ₐ[R] B) : LinearMap.mk f (map_smul f) = f.toLinearMap :=
  rfl

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