card_perms_of_finset

Mathlib.Data.Fintype.Perm

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

English

For any finset s, the number of permutations of its elements equals |s|!.

Русский

Для любого конечного множества s число перестановок его элементов равно |s|!.

LaTeX

$$$|\\mathrm{permsOfFinset}(s)| = |s|!$$$

Lean4

theorem card_perms_of_finset : ∀ s : Finset α, #(permsOfFinset s) = (#s)! := by rintro ⟨⟨l⟩, hs⟩;
  exact length_permsOfList l

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

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

Разделы

Аффилиация

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