is_cartan_of_zeroRootSubalgebra_eq

English

If the zero root subalgebra of H equals H, then H is a Cartan subalgebra.

Русский

Если нулевая корневая подсалалгебра H равна H, то H является картановой подалгеброй.

LaTeX

$$$\operatorname{zeroRootSubalgebra}(R,L,H) = H \Rightarrow H \text{ is CartanSubalgebra}$$$

Lean4

/-- If the zero root subalgebra of a nilpotent Lie subalgebra `H` is just `H` then `H` is a Cartan
subalgebra.

When `L` is Noetherian, it follows from Engel's theorem that the converse holds. See
`LieAlgebra.zeroRootSubalgebra_eq_iff_is_cartan` -/
theorem is_cartan_of_zeroRootSubalgebra_eq (h : zeroRootSubalgebra R L H = H) : H.IsCartanSubalgebra :=
  { nilpotent := inferInstance
    self_normalizing := by rw [← h]; exact zeroRootSubalgebra_normalizer_eq_self R L H }

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