Properties of Equiv.Perm on Finite types

theorem Nat.card_perm {α : Type u_1} [Finite α] : Nat.card (Equiv.Perm α) = (Nat.card α).factorial