Def Sylow.ofCard

Modification history

2024-07-17 06:20

Mathlib/GroupTheory/Sylow.lean

refactor(GroupTheory/PGroup,Sylow): Replace Fintype.card with Nat.card (#14789) …

Modified Sylow.ofCard View on Github →

2023-07-13 08:07

Mathlib/GroupTheory/Sylow.lean

feat(GroupTheory/Sylow): add inverse to card_eq_multiplicity (#5831) …

Added Sylow.ofCard View on Github →