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).