Theorem IsPGroup.cyclic_center_quotient_of_card_eq_prime_sq

Modification history

2024-07-17 06:20

Mathlib/GroupTheory/PGroup.lean

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

Modified IsPGroup.cyclic_center_quotient_of_card_eq_prime_sq View on Github →

2023-05-25 20:21

Mathlib/GroupTheory/PGroup.lean

feat: port GroupTheory.PGroup (#4318)

Added IsPGroup.cyclic_center_quotient_of_card_eq_prime_sq View on Github →