closureCommutatorRepresentatives_fg

Mathlib.GroupTheory.Commutator.Finite

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

English

The closure of the commutator representatives is a finitely generated group.

Русский

Замыкание представителей коммутаторов — это конечно порождаемая группа.

LaTeX

$$$\mathrm{Group.FG}(\mathrm{closureCommutatorRepresentatives}(G))$$$

Lean4

instance closureCommutatorRepresentatives_fg : Group.FG (closureCommutatorRepresentatives G) :=
  Group.closure_finite_fg _

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

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

Разделы

Аффилиация

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