toModuleHom_apply — Mathlib

English

The equality expressing that [I,N] is the range of the natural mapIncl followed by the action, i.e., (toModuleHom ∘ mapIncl I N).range.

Русский

Равенство, выражающее, что [I,N] является образом естественного отображения mapIncl, затем действием, то есть range (toModuleHom ∘ mapIncl I N).

LaTeX

$$$$ [I,N] = ((toModuleHom\;R\;L\;M) \circ (mapIncl\; I\; N)).range. $$$$

Lean4

@[simp]
theorem toModuleHom_apply (x : L) (m : M) : toModuleHom R L M (x ⊗ₜ m) = ⁅x, m⁆ := by
  simp only [toModuleHom, TensorProduct.LieModule.liftLie_apply, LieModuleHom.coe_mk, LieHom.coe_toLinearMap,
    toEnd_apply_apply]

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