nilpotent_of_mulEquiv — Mathlib

English

Nilpotence is preserved under group isomorphisms: if G is nilpotent and f is an isomorphism between G and G', then G' is nilpotent.

Русский

Нильпотентность сохраняется под групповыми изоморфизмами: если G нильпотентна и существует изоморфизм f: G ≅ G', то G' тоже нильпотентна.

LaTeX

$$$(G \\cong G') \\;\\Rightarrow\\; (\\operatorname{IsNilpotent}(G) \\Rightarrow \\operatorname{IsNilpotent}(G'))$$$

Lean4

/-- Nilpotency respects isomorphisms -/
theorem nilpotent_of_mulEquiv {G' : Type*} [Group G'] [_h : IsNilpotent G] (f : G ≃* G') : IsNilpotent G' :=
  nilpotent_of_surjective f.toMonoidHom (MulEquiv.surjective f)

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