commutator_apply

Mathlib.RingTheory.Derivation.Lie

URI: https://scilib.ai/kg/mathlib#Derivation.commutator_apply

English

For derivations D1 and D2, their bracket acts on an element a by D1(D2(a)) − D2(D1(a)).

Русский

Скобка производных действует на элемент a как D1(D2(a)) − D2(D1(a)).

LaTeX

$$$⁅D_1,D_2⁆(a) = D_1(D_2(a)) - D_2(D_1(a))\quad(a\in A).$$$

Lean4

theorem commutator_apply : ⁅D1, D2⁆ a = D1 (D2 a) - D2 (D1 a) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru