toLinearMap_comp — Mathlib

English

The composition of Lie algebra homomorphisms, viewed as linear maps, coincides with the usual linear map composition.

Русский

Композиция гомоморфизмов Ли, взятая как линейные отображения, совпадает с обычной композицией линейных отображений.

LaTeX

$$$ (f.comp g : L_1 \to_{\mathbb{R}} L_3) = (f : L_2 \to_{\mathbb{R}} L_3).comp (g : L_1 \to_{\mathbb{R}} L_2) $$$

Lean4

@[norm_cast, simp]
theorem toLinearMap_comp (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) :
    (f.comp g : L₁ →ₗ[R] L₃) = (f : L₂ →ₗ[R] L₃).comp (g : L₁ →ₗ[R] L₂) :=
  rfl

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