normalizer_eq_self_of_isCartanSubalgebra

English

If H is a Cartan subalgebra, then its normalizer as a Lie submodule equals itself.

Русский

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

LaTeX

$$$H^{\\text{normalizer}} = H$$$

Lean4

@[simp]
theorem normalizer_eq_self_of_isCartanSubalgebra (H : LieSubalgebra R L) [H.IsCartanSubalgebra] :
    H.toLieSubmodule.normalizer = H.toLieSubmodule := by
  rw [← LieSubmodule.toSubmodule_inj, coe_normalizer_eq_normalizer, IsCartanSubalgebra.self_normalizing,
    coe_toLieSubmodule]

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