lie_lie_smul_f

Mathlib.Algebra.Lie.Sl2

URI: https://scilib.ai/kg/mathlib#IsSl2Triple.lie_lie_smul_f

English

In an sl2-triple, the bracket [h,f] equals -2 f.

Русский

В sl2-тройке скобка [h,f] равна -2f.

LaTeX

$$[h,f] = -2 \cdot f$$

Lean4

theorem lie_lie_smul_f (t : IsSl2Triple h e f) : ⁅h, f⁆ = -((2 : R) • f) := by simp [t.lie_h_f_nsmul, two_smul]

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

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

Разделы

Аффилиация

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