ker_isPGroup_of_injective — Mathlib

English

If φ is injective, then its kernel is a p-group (trivial p-group).

Русский

Если гомоморфизм инъективен, то его ядро — p-группа (тривиальная).

LaTeX

$$$\ker \varphi \text{ is a } p\text{-group}$ when $\varphi$ is injective.$$

Lean4

theorem ker_isPGroup_of_injective {K : Type*} [Group K] {ϕ : K →* G} (hϕ : Function.Injective ϕ) : IsPGroup p ϕ.ker :=
  (congr_arg (fun Q : Subgroup K => IsPGroup p Q) (ϕ.ker_eq_bot_iff.mpr hϕ)).mpr IsPGroup.of_bot

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