derivedSeries_one

Mathlib.GroupTheory.Solvable

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

English

The first derived subgroup equals the commutator subgroup: D_1 = commutator(G).

Русский

Первый член производящей серии равен коммутаторной подгруппе: D_1 = commutator(G).

LaTeX

$$$\\mathrm{derivedSeries}(G,1) = \\mathrm{commutator}(G)$$$

Lean4

@[simp 1100]
theorem derivedSeries_one : derivedSeries G 1 = commutator G :=
  rfl

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

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

Разделы

Аффилиация

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