comap_of_injective — Mathlib

English

If H is a p-group and φ is injective, then H.comap φ is a p-group.

Русский

Если H — p-группа и φ инъективен, то H.comap φ — p-группа.

LaTeX

$$$\IsPGroup(p,H) \rightarrow (\varphi : K \to^* G) \rightarrow Function.Injective (MonoidHom) \rightarrow IsPGroup(p) (H.comap \varphi)$$$

Lean4

theorem comap_of_injective {H : Subgroup G} (hH : IsPGroup p H) {K : Type*} [Group K] (ϕ : K →* G)
    (hϕ : Function.Injective ϕ) : IsPGroup p (H.comap ϕ) :=
  hH.comap_of_ker_isPGroup ϕ (ker_isPGroup_of_injective hϕ)

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