nilpotent — Mathlib

English

A group G is nilpotent if and only if there exists an n with the nth upper central term equal to the whole group.

Русский

Группа G нильпотентна тогда и только тогда, когда существует некоторое n, для которого n-я ступень верхней центральной серии равна всей группе.

LaTeX

$$$\exists n:\mathbb{N},\ upperCentralSeries(G,n)=\top$$$

Lean4

theorem nilpotent (G : Type*) [Group G] [IsNilpotent G] : ∃ n : ℕ, upperCentralSeries G n = ⊤ :=
  Group.IsNilpotent.nilpotent'

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