card_perm

Mathlib.Data.Fintype.Perm

URI: https://scilib.ai/kg/mathlib#Fintype.card_perm

← MathLib Explorer

English

The number of permutations of a finite set of size n is n!.

Русский

Количества перестановок конечного множества размера n равна n!.

LaTeX

$$$Fintype.card(\\mathrm{Perm}(\\alpha)) = (Fintype.card \\alpha)!$$$

Lean4

theorem card_perm [Fintype α] : Fintype.card (Perm α) = (Fintype.card α)! :=
  Subsingleton.elim (@fintypePerm α _ _) (@Equiv.instFintype α α _ _ _ _) ▸ card_perms_of_finset _

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

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

Разделы

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

Аффилиация

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