instSMulNat — Mathlib

English

The commutator of two Lie derivations D1 and D2, when viewed as linear maps, corresponds to the commutator of their linear endomorphisms: ↑⁅D1, D2⁆ = ⁅(D1 : End_R(L)), (D2 : End_R(L))⁆.

Русский

Скобка-коммутатор двух Ли-производных D1 и D2, рассматриваемых как линейные отображения, соответствует коммутатору их линейных преобразований: ↑⁅D1, D2⁆ = ⁅(D1 : End_R(L)), (D2 : End_R(L))⁆.

LaTeX

$$$↑⁅D_1, D_2⁆ = ⁅(D_1 : \mathrm{End}_R L), (D_2 : \mathrm{End}_R L)⁆$$$

Lean4

instance instSMulNat : SMulBracketCommClass ℕ L M :=
  ⟨fun s l a => (lie_nsmul l a s).symm⟩

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