nilpotencyClass — Mathlib

English

The nilpotency class of a nilpotent group G is the smallest natural number n such that the nth term of the upper central series equals G.

Русский

Класс нильпотентности группы G есть наименьшее натуральное число n такое, что n-я степень верхней центральной серии равна всей группе G.

LaTeX

$$$\\mathrm{Group.nilpotencyClass}(G) = \\min\\{ n \\in \\mathbb{N} \\mid \\mathrm{upperCentralSeries}(G,n) = G \\}$$$

Lean4

/-- The nilpotency class of a nilpotent group is the smallest natural `n` such that
the `n`-th term of the upper central series is `G`. -/
noncomputable def nilpotencyClass : ℕ :=
  Nat.find (IsNilpotent.nilpotent G)

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