commutator_coe_linear_map — Mathlib

English

For derivations D1, D2, the bracket [D1, D2], viewed as a linear map, coincides with the commutator of their actions on End_R(A).

Русский

Для производных D1, D2 скобка [D1, D2], рассматриваемая как линейное отображение, совпадает с коммутатором их действий на End_R(A).

LaTeX

$$$\\uparrow\\llbracket D_1,D_2 \\rrbracket = \\llbracket (D_1 : \\mathrm{End}_R(A)), (D_2 : \\mathrm{End}_R(A) ) \\rrbracket$$$

Lean4

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

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