derivedSeries_zero

Mathlib.GroupTheory.Solvable

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

English

The 0th derived subgroup is the whole group: D_0 = ⊤.

Русский

Нулевой член производящей серии равен всей группе: D_0 = ⊤.

LaTeX

$$$\\mathrm{derivedSeries}(G,0) = \\top$$$

Lean4

@[simp]
theorem derivedSeries_zero : derivedSeries G 0 = ⊤ :=
  rfl

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

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

Разделы

Аффилиация

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