length_permutations — Mathlib

English

For any l ∈ List α, the number of permutations of l is (length l)!, i.e., the length of permutations l equals the factorial of the length of l.

Русский

Для любого списка l верно, что число перестановок l равно (length l)!, то есть длина permutations l равна факториалу длины l.

LaTeX

$$$$\operatorname{length}(\operatorname{permutations}\ l) = (\operatorname{length} l)!$$$$

Lean4

theorem length_permutations (l : List α) : length (permutations l) = (length l)! :=
  length_permutationsAux l []

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