instFintype

Mathlib.GroupTheory.SpecificGroups.Alternating

URI: https://scilib.ai/kg/mathlib#alternatingGroup.instFintype

English

If α is finite, then the alternating group on α is finite.

Русский

Пусть α конечно, тогда чередующаяся группа на α конечно.

LaTeX

$$$\operatorname{Fintype}(\mathrm{alternatingGroup}(\alpha))$$$

Lean4

instance instFintype : Fintype (alternatingGroup α) :=
  @Subtype.fintype _ _ sign.decidableMemKer _

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

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

Разделы

Аффилиация

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