instCoeOutLinearMapId — Mathlib

English

A Lie module homomorphism is a linear map in disguise; there is a canonical CoeOut to LinearMap.

Русский

Гомоморфизм модуля Ли трактуется как линейное отображение; существует каноническое преобразование в LinearMap.

LaTeX

$$$ \text{CoeOut} (M \to_{\mathsf{Lie}} N) (\text{LinearMap}) $$$

Lean4

instance : CoeOut (M →ₗ⁅R,L⁆ N) (M →ₗ[R] N) :=
  ⟨LieModuleHom.toLinearMap⟩

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