coe_normalizer_eq_normalizer — Mathlib

English

If H is a LieSubalgebra, then viewing H as a LieSubmodule, its normalizer coincides with H.normalizer.

Русский

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

LaTeX

$$$ (H^{\\text{toLieSubmodule}}).normalizer = H.normalizer $$$

Lean4

theorem coe_normalizer_eq_normalizer : (H.toLieSubmodule.normalizer : Submodule R L) = H.normalizer :=
  rfl

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