isNilpotent_congr — Mathlib

English

Nilpotence is preserved by group isomorphisms: if e: G ≃* H, then G is nilpotent iff H is nilpotent.

Русский

Нильпотентность сохраняется при групповом изоморфизме: если e: G ≃* H, то G нильпотентна тогда и только тогда, когда H нильпотентна.

LaTeX

$$$\text{IsNilpotent}(G) \iff \text{IsNilpotent}(H)$ for any isomorphism $e:G\to H$.$$

Lean4

theorem isNilpotent_congr {H : Type*} [Group H] (e : G ≃* H) : IsNilpotent G ↔ IsNilpotent H :=
  by
  simp_rw [isNilpotent_iff]
  refine exists_congr fun n ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · simp [← Subgroup.comap_top e.symm.toMonoidHom, ← h]
  · simp [← Subgroup.comap_top e.toMonoidHom, ← h]

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