comap_normalizer — Mathlib

English

For a LieModuleHom f: M' →ₗ⁅R,L⁆ M, the normalizer commutes with comap: N.normalizer.comap f = (N.comap f).normalizer.

Русский

Для гомоморфизма модуля Ли f: M' →ₗ⁅R,L⁆ M нормализатор коммутирует с обратным образом: N.normalizer.comap f = (N.comap f).normalizer.

LaTeX

$$$ N.normalizer.comap f = (N.comap f).normalizer $$$

Lean4

@[simp]
theorem comap_normalizer (f : M' →ₗ⁅R,L⁆ M) : N.normalizer.comap f = (N.comap f).normalizer := by ext; simp

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