ideal_in_normalizer — Mathlib

English

The normalizer is a monotone operator on Lie submodules: if N1 ≤ N2 then N1.normalizer ≤ N2.normalizer.

Русский

Нормализатор — монотонный оператор на Ли-подмодулях: если N1 ⊆ N2, то N1.normalizer ⊆ N2.normalizer.

LaTeX

$$$ N_1 \\le N_2 \\Rightarrow N_1.normalizer \\le N_2.normalizer $$$

Lean4

/-- A Lie subalgebra is an ideal of its normalizer. -/
theorem ideal_in_normalizer {x y : L} (hx : x ∈ H.normalizer) (hy : y ∈ H) : ⁅x, y⁆ ∈ H :=
  by
  rw [← lie_skew, neg_mem_iff (G := L)]
  exact hx ⟨y, hy⟩

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