coe_toLinearMap — Mathlib

English

The function obtained by coercing a LieModuleHom to LinearMap, and then projecting to functions, equals the original function from f.

Русский

Переход от LieModuleHom к LinearMap сохраняет функцию; полученная функция совпадает с исходной.

LaTeX

$$$ (f : M \to_{\mathsf{Lie}} N) : M \to N = f.toLinearMap $$$

Lean4

@[simp, norm_cast]
theorem coe_toLinearMap (f : M →ₗ⁅R,L⁆ N) : ((f : M →ₗ[R] N) : M → N) = f :=
  rfl

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