length_permsOfList — Mathlib

English

For any list l, the number of permutations of its elements equals factorial(length l).

Русский

Для любого списка l количество перестановок элементов равно факториалу длины l.

LaTeX

$$$|\\mathrm{permsOfList}(l)| = |l|!$$$

Lean4

theorem length_permsOfList : ∀ l : List α, length (permsOfList l) = l.length !
  | [] => rfl
  | a :: l => by simp [Nat.factorial_succ, permsOfList, length_permsOfList, succ_mul, add_comm]

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