normalizerCondition_iff_only_full_group_self_normalizing

English

Normalier condition is equivalent to every normalizer being left unchanged by all automorphisms.

Русский

Условие нормализатора эквивалентно тому, что нормализатор остаётся фиксированным под всеми автоморфизмами.

LaTeX

$$$Normalizers(G) \iff \forall H, H.normalizer = H$ under automorphisms.$$

Lean4

/-- Alternative phrasing of the normalizer condition: Only the full group is self-normalizing.
This may be easier to work with, as it avoids inequalities and negations. -/
theorem _root_.normalizerCondition_iff_only_full_group_self_normalizing :
    NormalizerCondition G ↔ ∀ H : Subgroup G, H.normalizer = H → H = ⊤ :=
  by
  apply forall_congr'; intro H
  simp only [lt_iff_le_and_ne, le_normalizer, le_top, Ne]
  tauto

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