English
If ker f is a p-group and Sylow p G is finite, then Sylow p H is finite (for any domain H).
Русский
Если ядро f является p-группой, и Sylow p G конечно, то Sylow p H конечно (для любого домена H).
LaTeX
$$$ IsPGroup\\ p\\ (f.ker) \\Rightarrow [Finite (Sylow p G)] \\Rightarrow [Finite (Sylow p H)]$$$
Lean4
/-- If the kernel of `f : H →* G` is a `p`-group,
then `Finite (Sylow p G)` implies `Finite (Sylow p H)`. -/
theorem finite_of_ker_is_pGroup {H : Type*} [Group H] {f : H →* G} (hf : IsPGroup p f.ker) [Finite (Sylow p G)] :
Finite (Sylow p H) :=
let h_exists := fun P : Sylow p H => P.exists_comap_eq_of_ker_isPGroup hf
let g : Sylow p H → Sylow p G := fun P => Classical.choose (h_exists P)
have hg : ∀ P : Sylow p H, (g P).1.comap f = P := fun P => Classical.choose_spec (h_exists P)
Finite.of_injective g fun P Q h => ext (by rw [← hg, h]; exact (h_exists Q).choose_spec)
