English
The Cartan subalgebra, as a Lie module over itself, admits a triangularization; concretely, there exists a basis making the diagonal action explicit in the triangular form for the corresponding Lie module.
Русский
Картанова подалгебра как модуль по самому себе допускает треугольное разложение; существует базис, в котором действие диагонально и в треугольной форме.
LaTeX
$$LieModule.IsTriangularizable(cartanSubalgebra'(b), ...)$$
Lean4
instance : IsLieAbelian (cartanSubalgebra' b) :=
by
refine ⟨fun ⟨⟨x, hx⟩, hx'⟩ ⟨⟨y, hy⟩, hy'⟩ ↦ ?_⟩
let x' : cartanSubalgebra b := ⟨x, hx'⟩
let y' : cartanSubalgebra b := ⟨y, hy'⟩
suffices ⁅x', y'⁆ = 0 by simpa [x', y', Subtype.ext_iff, -trivial_lie_zero] using this
simp
