Commit 2024-06-05 07:22 b00b6e0f

View on Github →

feat(GroupTheory/Frattini): definition and first theorem (#13418) We give the definition of the Frattini subgroup of a group, and three elementary results:

The Frattini subgroup is characteristic.
If every subgroup of a group is contained in a maximal subgroup, then the Frattini subgroup consists of the non-generating elements of the group.
The Frattini subgroup of a finite group is nilpotent.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Subgroup/Basic.lean

added def MulEquiv.comapSubgroup

added theorem MulEquiv.isCoatom_comap

added theorem MulEquiv.isCoatom_map

added def MulEquiv.mapSubgroup

modified theorem Subgroup.Normal.comap

added theorem Subgroup.Normal.of_map_injective

added theorem Subgroup.Normal.of_map_subtype

modified theorem Subgroup.Normal.subgroupOf

modified theorem Subgroup.comap_normalClosure

added theorem Subgroup.isCoatom_comap_of_surjective

modified theorem Subgroup.map_normalClosure

Created Mathlib/GroupTheory/Frattini.lean

added def frattini

added theorem frattini_le_coatom

added theorem frattini_le_comap_frattini_of_surjective

added theorem frattini_nilpotent

added theorem frattini_nongenerating

Created Mathlib/Order/Radical.lean

added def Order.radical

added theorem Order.radical_le_coatom

added theorem Order.radical_nongenerating

added theorem OrderIso.map_radical