toLieHom_comp — Mathlib

English

LieHom corresponding to the composition of AlgHoms equals the composition of the corresponding LieHoms.

Русский

LieHom, соответствующий композиции AlgHom, равен композиции соответствующих LieHom.

LaTeX

$$$$ (g \circ f)^{\mathrm{Lie}} = g^{\mathrm{Lie}} \circ f^{\mathrm{Lie}}. $$$$

Lean4

@[simp]
theorem toLieHom_comp : (g.comp f : A →ₗ⁅R⁆ C) = (g : B →ₗ⁅R⁆ C).comp (f : A →ₗ⁅R⁆ B) :=
  rfl

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