Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes