exists_comap_eq_of_injective — Mathlib

English

If f is injective, then there exists Q : Sylow p G with Q.comap f = P.

Русский

Если f инъективен, существует Q : Sylow p G такой, что Q.comap f = P.

LaTeX

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

Lean4

theorem exists_comap_eq_of_injective {H : Type*} [Group H] (P : Sylow p H) {f : H →* G} (hf : Function.Injective f) :
    ∃ Q : Sylow p G, Q.comap f = P :=
  P.exists_comap_eq_of_ker_isPGroup (IsPGroup.ker_isPGroup_of_injective hf)

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