coe_toLieModuleHom — Mathlib

English

The underlying map of e when viewed as a LieModuleHom equals e itself; the representation as a Lie module hom preserves the function.

Русский

У отображения e при рассмотрении как отображения Ли-модуля и превращении в тензорное отображение функция совпадает с самой e.

LaTeX

$$$\\bigl(e : M \\to N\\bigr) = e$$$

Lean4

theorem coe_toLieModuleHom (e : M ≃ₗ⁅R,L⁆ N) : ⇑(e : M →ₗ⁅R,L⁆ N) = e :=
  rfl

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