Theorem not_dvd_index_sylow'

Modification history

2024-11-07 22:07
Mathlib/GroupTheory/Sylow.lean
refactor(GroupTheory/Sylow): Add version of `Sylow.not_dvd_index` with only typeclass assumptions (#18572) …
Deleted not_dvd_index_sylow'View on Github →
2023-05-29 09:35
Mathlib/GroupTheory/Sylow.lean
feat: port GroupTheory.Sylow (#4387)
Added not_dvd_index_sylow'View on Github →