mathlib
dc766dd4 - refactor(group_theory/sylow): Golf proof of `pow_dvd_card_of_pow_dvd_card` (#14622)

Commit

3 years ago

refactor(group_theory/sylow): Golf proof of `pow_dvd_card_of_pow_dvd_card` (#14622) This PR golfs the proof of `pow_dvd_card_of_pow_dvd_card`.

Author

tb65536

Parents