normalizer_eq_top_iff — Mathlib

English

For any subgroup H of G, H.normalizer = ⊤ if and only if H is a normal subgroup of G.

Русский

Для любой подгруппы H группы G, H.normalizer = ⊤ тогда и только тогда, когда H является нормальной подгруппой G.

LaTeX

$$$H \trianglelefteq G \iff H.\operatorname{normalizer} = \top$$$

Lean4

@[to_additive]
theorem normalizer_eq_top_iff : H.normalizer = ⊤ ↔ H.Normal :=
  eq_top_iff.trans
    ⟨fun h => ⟨fun a ha b => (h (mem_top b) a).mp ha⟩, fun h a _ha b =>
      ⟨fun hb => h.conj_mem b hb a, fun hb => by rwa [h.mem_comm_iff, inv_mul_cancel_left] at hb⟩⟩

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