frattini — Mathlib

English

The Frattini subgroup of a group G is the intersection of all maximal subgroups of G.

Русский

Фраттини-подгруппа группы G есть пересечение всех максимальных подгрупп G.

LaTeX

$$$\\operatorname{frattini}(G) = \\bigcap_{M\\le G,\\; M \\text{ maximal}} M$$$

Lean4

/-- The Frattini subgroup of a group is the intersection of the maximal subgroups. -/
def frattini (G : Type*) [Group G] : Subgroup G :=
  Order.radical (Subgroup G)

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