Commit 2021-09-06 12:25 e8fff266
View on Github →refactor(group_theory/*): Move Cauchy's theorem (#8916)
Moves Cauchy's theorem from sylow.lean to perm/cycle_type.lean. Now perm/cycle_type.lean no longer depends on sylow.lean, and p_group.lean can use Cauchy's theorem (e.g. for equivalent characterizations of p-groups).