card_alternatingGroup

Mathlib.GroupTheory.SpecificGroups.Alternating

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

← MathLib Explorer

English

For nontrivial α, card(Alt(α)) = (card α)! / 2.

Русский

Для ненулевого α выполняется |Alt(α)| = |α|! / 2.

LaTeX

$$$\mathrm{card}(\mathrm{alternatingGroup}(\alpha)) = \dfrac{(\mathrm{card}(\alpha))!}{2}$$$

Lean4

theorem card_alternatingGroup [Nontrivial α] : card (alternatingGroup α) = (card α).factorial / 2 :=
  Nat.eq_div_of_mul_eq_right two_ne_zero (two_mul_card_alternatingGroup.trans card_perm)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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