frattini_le_coatom

Mathlib.GroupTheory.Frattini

URI: https://scilib.ai/kg/mathlib#frattini_le_coatom

English

If K is a coatom (a maximal proper subgroup) of G, then the Frattini subgroup is contained in K.

Русский

Если K является коатомом (максимальной собственно-подгруппой) G, то Frattini(G) ⊆ K.

LaTeX

$$$\\text{IsCoatom}(K) \\Rightarrow \\operatorname{frattini}(G) \\le K$$$

Lean4

theorem frattini_le_coatom {K : Subgroup G} (h : IsCoatom K) : frattini G ≤ K :=
  Order.radical_le_coatom h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru