Theorems · Definition · group theory
MonoidHom.transferSylow
{G : Type u_1} →
[inst : Group G] →
{p : ℕ} → (P : Sylow p G) → Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P → [(↑P).FiniteIndex] → G →* ↥↑PThe homomorphism G →* P in Burnside's transfer theorem.
- Defined in
- Mathlib.GroupTheory.Transfer
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- GroupSubgroup.FiniteIndex
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SetLike.coestatement and proof · cited by 8,199
- Groupstatement and proof · cited by 6,238
- MonoidHomstatement · cited by 3,629
- Subgroupstatement · cited by 3,593
- MonoidHom.idproof · cited by 323
- Subgroup.FiniteIndexstatement and proof · cited by 113
- Subgroup.normalizerstatement and proof · cited by 108
- Sylowstatement and proof · cited by 103
- Sylow.toSubgroupstatement and proof · cited by 86
- Subgroup.centralizerstatement and proof · cited by 65
- MonoidHom.transferproof · cited by 6
Cited by9
Results whose statement or proof uses this declaration.
- MonoidHom.ker_transferSylow_isComplement'statement and proof · cited by 3
- MonoidHom.transferSylow_domRestrict_eq_powstatement · cited by 2
- IsCyclic.isComplement'statement and proof · cited by 1
- MonoidHom.transferSylow_eq_powstatement · cited by 1
- MonoidHom.not_dvd_card_ker_transferSylowstatement · cited by 1
- Sylow.not_dvd_card_commutator_or_not_dvd_index_commutatorproof · cited by 1
- IsZGroup.commutator_ltproof · cited by 0
- MonoidHom.ker_transferSylow_disjointstatement and proof · cited by 0
- MonoidHom.transferSylow_restrict_eq_powstatement · cited by 0