of_surjective — Mathlib

English

Let p be a natural number. If G is a p-group and φ: G → H is a surjective group homomorphism, then H is a p-group.

Русский

Пусть p — натуральное число. Если G — p-группа и φ: G → H — сюръективный групповый гомоморфизм, то H — p-группа.

LaTeX

$$$\IsPGroup(p,G) \rightarrow \forall H [Group H] (\varphi : G \to^* H), \operatorname{Surjective}(\varphi) \rightarrow \IsPGroup(p,H)$$$

Lean4

theorem of_surjective {H : Type*} [Group H] (ϕ : G →* H) (hϕ : Function.Surjective ϕ) : IsPGroup p H :=
  by
  refine fun h => Exists.elim (hϕ h) fun g hg => Exists.imp (fun k hk => ?_) (hG g)
  rw [← hg, ← ϕ.map_pow, hk, ϕ.map_one]

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