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)