idealizer_eq_normalizer — Mathlib

English

For any LieIdeal I of L, its idealizer equals its normalizer: I.idealizer = I.normalizer.

Русский

Для любого Ли-идеала I в L, его идеалайзер равен нормализатору: I.idealizer = I.normalizer.

LaTeX

$$$ I.idealizer = I.normalizer $$$

Lean4

@[simp]
theorem _root_.LieIdeal.idealizer_eq_normalizer (I : LieIdeal R L) : I.idealizer = I.normalizer := by ext x;
  exact forall_congr' fun y ↦ by simp only [← lie_skew x y, neg_mem_iff]

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