English
In Burnside's transfer theorem context, there is a transfer homomorphism from G to a Sylow p-subgroup P, built using a compatible commutative group construction.
Русский
В контексте теоремы переноса Ферма-Бернсайда существует гомоморфизм переноса G →* P, где P — подгруппа Силова, построенный с помощью совместной конструкций коммутативной группы.
LaTeX
$$$\mathrm{transferSylow}: G \to* P$ with suitable normalizer-centralizer compatibility$$
Lean4
/-- The homomorphism `G →* P` in Burnside's transfer theorem. -/
noncomputable def transferSylow [FiniteIndex (P : Subgroup G)] : G →* (P : Subgroup G) :=
@transfer G _ P P (@CommGroup.ofIsMulCommutative P _ ⟨⟨fun a b => Subtype.ext (hP (le_normalizer b.2) a a.2)⟩⟩)
(MonoidHom.id P) _
