isNilpotent_top — Mathlib

English

A group G is nilpotent iff its top subgroup, viewed as G itself, is nilpotent.

Русский

Группа G нильпотентна тогда, когда её верхняя подгруппа тождественно равна G и сама нильпотентна.

LaTeX

$$$\text{IsNilpotent}(\top\text{ Subgroup }G) \iff \text{IsNilpotent}(G)$$$

Lean4

@[simp]
theorem isNilpotent_top : IsNilpotent (⊤ : Subgroup G) ↔ IsNilpotent G :=
  isNilpotent_congr Subgroup.topEquiv

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