ucs_le_of_normalizer_eq_self — Mathlib

English

If N1.normalizer = N1, then for all k, N1.ucs k ≤ ⊥ (inferred from context) or more precisely ≤ N1.

Русский

Если N1.normalizer = N1, то для любого k N1.ucs k ≤ N1.

LaTeX

$$$\\forall k, N_1.ucs k \\le N_1.$$$

Lean4

/-- If a Lie module `M` contains a self-normalizing Lie submodule `N`, then all terms of the upper
central series of `M` are contained in `N`.

An important instance of this situation arises from a Cartan subalgebra `H ⊆ L` with the roles of
`L`, `M`, `N` played by `H`, `L`, `H`, respectively. -/
theorem ucs_le_of_normalizer_eq_self (h : N₁.normalizer = N₁) (k : ℕ) : (⊥ : LieSubmodule R L M).ucs k ≤ N₁ :=
  by
  rw [← ucs_eq_self_of_normalizer_eq_self h k]
  gcongr
  simp

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