Frattini

📁 Source: Mathlib/GroupTheory/Frattini.lean

Statistics

Metric	Count
Definitions frattini	1
Theorems frattini_characteristic, frattini_le_coatom, frattini_le_comap_frattini_of_surjective, frattini_nilpotent, frattini_nongenerating	5
Total	6

(root)

Definitions

Name	Category	Theorems
frattini 📖	CompOp	4 math math: frattini_le_comap_frattini_of_surjective, frattini_le_coatom, frattini_characteristic, frattini_nilpotent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
frattini_characteristic 📖	mathematical	—	Subgroup.Characteristic frattini	—	Subgroup.characteristic_iff_comap_eq OrderIso.map_radical
frattini_le_coatom 📖	mathematical	IsCoatom Subgroup PartialOrder.toPreorder Subgroup.instPartialOrder BoundedOrder.toOrderTop Preorder.toLE CompleteLattice.toBoundedOrder Subgroup.instCompleteLattice	frattini	—	Order.radical_le_coatom
frattini_le_comap_frattini_of_surjective 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder frattini Subgroup.comap	—	Subgroup.comap_iInf biInf_le Subgroup.isCoatom_comap_of_surjective
frattini_nilpotent 📖	mathematical	—	Group.IsNilpotent Subgroup SetLike.instMembership Subgroup.instSetLike frattini Subgroup.toGroup	—	List.TFAE.out isNilpotent_of_finite_tfae Subgroup.instFiniteSubtypeMem Sylow.normalizer_sup_eq_top Subgroup.normal_of_characteristic frattini_characteristic Sylow.instFiniteSubtypeMemSubgroup SetLike.instFinite frattini_nongenerating IsStronglyCoatomic.toIsCoatomic instIsStronglyCoatomicOfWellFoundedGT Finite.to_wellFoundedGT Subgroup.normalizer_eq_top_iff Subgroup.Normal.of_map_subtype
frattini_nongenerating 📖	—	Subgroup SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Subgroup.instCompleteLattice frattini Top.top Subgroup.instTop	—	—	Order.radical_nongenerating

---

← Back to Index