of_injective — Mathlib

English

If IsPGroup p G and ϕ: H → G is an injective homomorphism, then IsPGroup p H.

Русский

Если G является p-группой и ϕ: H → G — инъективный гомоморфизм, тогда H — p-группа.

LaTeX

$$IsPGroup p H := IsPGroup p G (via injective ϕ)$$

Lean4

theorem of_injective {H : Type*} [Group H] (ϕ : H →* G) (hϕ : Function.Injective ϕ) : IsPGroup p H :=
  by
  simp_rw [IsPGroup, ← hϕ.eq_iff, ϕ.map_pow, ϕ.map_one]
  exact fun h => hG (ϕ h)

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