instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra

English

There is an instance declaring that the Cartan subalgebra, as a subtype of the ambient matrix Lie algebra, is LieAbelian.

Русский

Существует инстанс, объявляющий, что Картанова подалгебра, как подтип в окружающую матричную Ли-алгебру, является абелевой.

LaTeX

$$IsLieAbelian(cartanSubalgebra'(b))$$

Lean4

instance : IsLieAbelian (cartanSubalgebra b) :=
  by
  rw [cartanSubalgebra_eq_lieSpan, LieSubalgebra.isLieAbelian_lieSpan_iff]
  rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩
  exact lie_h_h i j

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