of_quotient_center_nilpotent — Mathlib

English

If G/Z(G) is nilpotent, then G is nilpotent.

Русский

Если G/Z(G) нильпотентна, то сама G нильпотентна.

LaTeX

$$$\\operatorname{IsNilpotent}(G/Z(G)) \\Rightarrow \\operatorname{IsNilpotent}(G)$$$

Lean4

/-- If the quotient by `center G` is nilpotent, then so is G. -/
theorem of_quotient_center_nilpotent (h : IsNilpotent (G ⧸ center G)) : IsNilpotent G :=
  by
  obtain ⟨n, hn⟩ := h.nilpotent
  use n.succ
  simp [← comap_upperCentralSeries_quotient_center, hn]

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