Theorem: ex_1_2_10_i (AlgebraI/Subgroups.lean)

State before:
n : ℕ
⊢ Nat.card (Equiv.Perm (Fin n)) = n !
Tactic:
rw [Nat.card_eq_fintype_card, Fintype.card_perm, Fintype.card_fin]
State after:
no goals