exists_comap_eq_of_ker_isPGroup — Mathlib

English

There exists Q : Sylow p G such that Q.comap f = P when ker f is a p-group and P ≤ range f.

Русский

Существет Q : Sylow p G such that Q.comap f = P, если ker f — p-подгруппа и P ≤ range f.

LaTeX

$$$\\exists Q : Sylow p G, Q.comap f = P$$$

Lean4

theorem exists_comap_eq_of_ker_isPGroup {H : Type*} [Group H] (P : Sylow p H) {f : H →* G} (hf : IsPGroup p f.ker) :
    ∃ Q : Sylow p G, Q.comap f = P :=
  Exists.imp (fun Q hQ => P.3 (Q.2.comap_of_ker_isPGroup f hf) (map_le_iff_le_comap.mp hQ)) (P.2.map f).exists_le_sylow

Похожие утверждения