upperCentralSeries_isAscendingCentralSeries

Mathlib.GroupTheory.Nilpotent

URI: https://scilib.ai/kg/mathlib#upperCentralSeries_isAscendingCentralSeries

← MathLib Explorer

English

Another articulation: IsAscendingCentralSeries (upperCentralSeries G).

Русский

Другое утверждение: IsAscendingCentralSeries (upperCentralSeries G).

LaTeX

$$$\text{IsAscendingCentralSeries}(\mathrm{upperCentralSeries}(G))$$$

Lean4

/-- The upper central series of a group is an ascending central series. -/
theorem upperCentralSeries_isAscendingCentralSeries : IsAscendingCentralSeries (upperCentralSeries G) :=
  ⟨rfl, fun _x _n h => h⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru