mathlib
e8fff266 - refactor(group_theory/*): Move Cauchy's theorem (#8916)

Commit
4 years ago
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).
Author
Parents
Loading