of_equiv — Mathlib

English

If G is a p-group, then H is a p-group whenever G and H are isomorphic via a group isomorphism.

Русский

Если G — p-группа, то H — p-группа, если G и H изоморфны через изоморфизм групп.

LaTeX

$$$\IsPGroup(p,G) \rightarrow \forall H [Group H] (\varphi: G \simeq H), \IsPGroup(p,H)$$$

Lean4

theorem of_equiv {H : Type*} [Group H] (ϕ : G ≃* H) : IsPGroup p H :=
  hG.of_surjective ϕ.toMonoidHom ϕ.surjective

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