ucs_eq_self_of_isCartanSubalgebra

English

For a Cartan subalgebra H, the k-th step of the upper central series equals H for every k.

Русский

Для картановой подалгебры H верхняя центральная последовательность фиксируется на H на любом шаге.

LaTeX

$$$\\forall k:\\; \\text{L Submodule}.ucs_k(H) = H$$$

Lean4

@[simp]
theorem ucs_eq_self_of_isCartanSubalgebra (H : LieSubalgebra R L) [H.IsCartanSubalgebra] (k : ℕ) :
    H.toLieSubmodule.ucs k = H.toLieSubmodule := by
  induction k with
  | zero => simp
  | succ k ih => simp [ih]

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