zeroRootSubalgebra_eq_iff_is_cartan

English

For any H, the zero root subalgebra equals H if and only if H is CartanSubalgebra.

Русский

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

LaTeX

$$$\operatorname{zeroRootSubalgebra}(R,L,H) = H \iff H.IsCartanSubalgebra$$$

Lean4

theorem zeroRootSubalgebra_eq_iff_is_cartan [IsNoetherian R L] : zeroRootSubalgebra R L H = H ↔ H.IsCartanSubalgebra :=
  ⟨is_cartan_of_zeroRootSubalgebra_eq R L H, by intros; simp⟩

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