normal_of_coatom — Mathlib

English

If a group G has the normalizer condition and H is a maximal (coat) subgroup of G, then H is normal in G.

Русский

Пусть группа G удовлетворяет условию нормализатора; если H — максимальная подпгруппа G, то H нормальна в G.

LaTeX

$$Normal( H\;|\;IsCoatom(H)\Rightarrow H\trianglelefteq G )$$

Lean4

/-- In a group that satisfies the normalizer condition, every maximal subgroup is normal -/
theorem normal_of_coatom (hnc : NormalizerCondition G) (hmax : IsCoatom H) : H.Normal :=
  normalizer_eq_top_iff.mp (hmax.2 _ (hnc H (lt_top_iff_ne_top.mpr hmax.1)))

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