lie_h_e_smul

Mathlib.Algebra.Lie.Sl2

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

English

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

Русский

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

LaTeX

$$[h,e] = 2 \cdot e$$

Lean4

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

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

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

Разделы

Аффилиация

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