instFiniteElemProdCommutatorRepresentatives

Mathlib.GroupTheory.Commutator.Finite

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

English

The set of commutator representatives is finite.

Русский

Множество представителей коммутаторов конечно.

LaTeX

$$$\mathrm{Finite}(\mathrm{commutatorRepresentatives}(G))$$$

Lean4

instance : Finite (commutatorRepresentatives G) :=
  Set.finite_coe_iff.mpr (Set.finite_range _)

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

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

Разделы

Аффилиация

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