sl2SubalgebraOfRoot — Mathlib

English

There is an embedded sl2-subalgebra corresponding to α contained in L.

Русский

Существует вложенная подалгебра sl₂, соответствующая α, внутри L.

LaTeX

$$sl2SubalgebraOfRoot α ⊆ L$$

Lean4

/-- The embedded `sl₂` associated to a root. -/
noncomputable def sl2SubalgebraOfRoot {α : Weight K H L} (hα : α.IsNonZero) : LieSubalgebra K L :=
  by
  choose h e f t ht using exists_isSl2Triple_of_weight_isNonZero hα
  exact t.toLieSubalgebra K

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