commutator_coe_linear_map — Mathlib

English

The commutator of two Lie derivations, when viewed as linear maps, equals the commutator of their linear maps: ↑⁅D1, D2⁆ = ⁅(D1 : Linear End), (D2 : Linear End)⁆.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem commutator_coe_linear_map : ↑⁅D1, D2⁆ = ⁅(D1 : Module.End R L), (D2 : Module.End R L)⁆ :=
  rfl

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