Fintype.card_perm

theorem Fintype.card_perm : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α], Fintype.card (Equiv.Perm α) = (Fintype.card α).factorial

The theorem `Fintype.card_perm` states that for any type `α` that has decidable equality and is a finite type, the number of bijections (permutations) from `α` to itself is equal to the factorial of the number of elements in `α`. In mathematical terms, if `α` is a finite set then the number of permutations of `α` is `n!` where `n` is the cardinality of `α`.

More concisely: For a finite type `α` with decidable equality, the number of bijections from `α` to itself is equal to the factorial of its cardinality.