Commit 2024-11-07 22:07 2f04ff05
View on Github →refactor(GroupTheory/Sylow): Add version of Sylow.not_dvd_index with only typeclass assumptions (#18572)
This PR adds a version of Sylow.not_dvd_index with only typeclass assumptions since in practice it is applied to finite groups where the typeclass assumptions can be inferred automatically. This allows for a little golfing in Transfer.lean.