Theorems · Definition · group theory
Sylow.toSubgroup
{p : ℕ} → {G : Type u_1} → [inst : Group G] → Sylow p G → Subgroup G- Defined in
- Mathlib.GroupTheory.Sylow
- Cited by
- 86 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by100
Results whose statement or proof uses this declaration.
- Sylow.isPGroup'statement · cited by 19
- Sylow.subtypestatement and proof · cited by 10
- MonoidHom.transferSylowstatement and proof · cited by 9
- Sylow.not_dvd_indexstatement and proof · cited by 9
- Sylow.is_maximal'statement · cited by 6
- Sylow.coe_coestatement · cited by 5
- Sylow.ext_iffstatement and proof · cited by 5
- alternatingGroup.two_sylow_eq_kleinFour_of_card_eq_fourstatement and proof · cited by 4
- Sylow.coe_subtypestatement and proof · cited by 4
- Sylow.mapSurjectiveproof · cited by 4
- Sylow.extstatement and proof · cited by 3
- MonoidHom.ker_transferSylow_isComplement'statement and proof · cited by 3