Mathlib

1/4

A permutation is a bijection {1,…,n} → {1,…,n}. Count: n choices, then n−1, …