LieAlgebra.is_cartan_of_zeroRootSubalgebra_eq

theorem LieAlgebra.is_cartan_of_zeroRootSubalgebra_eq : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (H : LieSubalgebra R L) [inst_3 : LieAlgebra.IsNilpotent R ↥H], LieAlgebra.zeroRootSubalgebra R L H = H → H.IsCartanSubalgebra

The theorem states that for a given nilpotent Lie subalgebra `H` of a Lie algebra `L` over a commutative ring `R`, if the zero root subalgebra of `H` is equal to `H` itself, then `H` is a Cartan subalgebra. In other words, if the subalgebra generated by the root space of the zero map from `H` to `R` is just `H`, then `H` has the properties of a Cartan subalgebra. It's worth noting that if `L` is Noetherian, the converse of this theorem also holds true according to Engel's theorem, as mentioned in the theorem `LieAlgebra.zeroRootSubalgebra_eq_iff_is_cartan`.

More concisely: If a nilpotent Lie subalgebra `H` of a Lie algebra `L` over a commutative ring `R` has the property that its zero root subalgebra equals `H`, then `H` is a Cartan subalgebra. (Assuming `L` is Noetherian, the converse also holds by Engel's theorem.)