subgroupOf_normalizer_eq — Mathlib

English

For subgroups H ≤ N, the normalizer of H in G extended to N equals the normalizer of H in N via subgroupOf.

Русский

Для подгрупп H ≤ N нормализатор H внутри G, ограниченный до N, равен нормализатору H в N через subgroupOf.

LaTeX

$$$H \le N \Rightarrow H.\mathrm{normalizer}^G = (H.\mathrm{subgroupOf}N).\mathrm{normalizer}$$$

Lean4

@[to_additive]
theorem subgroupOf_normalizer_eq {H N : Subgroup G} (h : H ≤ N) :
    H.normalizer.subgroupOf N = (H.subgroupOf N).normalizer :=
  comap_normalizer_eq_of_le_range (h.trans_eq N.range_subtype.symm)

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