coe_maxTrivEquiv_apply — Mathlib

English

The map maxTrivHom is linear and respects Lie bracket, hence is a LieModuleHom between the maximal trivial submodules.

Русский

Отображение maxTrivHom линейно и сохраняет скобку Ли, следовательно, является гомоморфизмом модуля Ли между максимальными тривиальными подмодулями.

LaTeX

$$$\\text{maxTrivHom } f \\text{ is a LieModuleHom}$$$

Lean4

@[norm_cast, simp]
theorem coe_maxTrivEquiv_apply (e : M ≃ₗ⁅R,L⁆ N) (m : maxTrivSubmodule R L M) : (maxTrivEquiv e m : N) = e ↑m :=
  rfl

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