map — Mathlib

English

The image of a p-group under a group homomorphism is a p-group.

Русский

Образ p-группы под гомоморфизмом группы — p-группа.

LaTeX

$$$\forall {H : Subgroup G} (hH : IsPGroup p H) {K : Type*} [Group K] (\varphi : G \to^* K), IsPGroup p (H.map \varphi)$$$

Lean4

theorem map {H : Subgroup G} (hH : IsPGroup p H) {K : Type*} [Group K] (ϕ : G →* K) : IsPGroup p (H.map ϕ) :=
  by
  rw [← H.range_subtype, MonoidHom.map_range]
  exact hH.of_surjective (ϕ.restrict H).rangeRestrict (ϕ.restrict H).rangeRestrict_surjective

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