Commit 2026-07-16 05:00 c26b2a17

View on Github →

feat(GroupTheory/PGroup): expand p-group API (#40143) Basic properties and iffs with orderOf/Nat.card/Monoid.exponent.

Estimated changes

Modified Mathlib/GroupTheory/PGroup.lean

modified theorem IsPGroup.iff_orderOf

added theorem IsPGroup.isOfFinOrder

modified theorem IsPGroup.of_card

added theorem IsPGroup.of_card_dvd_pow

added theorem IsPGroup.of_exponent_dvd_pow

added theorem IsPGroup.of_pow

added theorem IsPGroup.of_subsingleton

added theorem isPGroup_iff_card_dvd_pow

added theorem isPGroup_iff_exists_orderOf_dvd_pow

added theorem isPGroup_iff_exists_pow_pow_eq_one

added theorem isPGroup_iff_exponent_dvd_pow

added theorem isPGroup_iff_exponent_eq_pow

added theorem isPGroup_iff_isPGroup_prod_primeFactors

added theorem isPGroup_iff_orderOf_dvd_pow

added theorem isPGroup_iff_pow_pow_eq_one

added theorem isPGroup_iff_primeFactors_card_subset

added theorem isPGroup_one_iff_subsingleton

Modified Mathlib/GroupTheory/Sylow.lean

added theorem Sylow.coe_equivProdPrimeFactors_apply

added theorem Sylow.coe_symm_equivProdPrimeFactors_apply

added theorem Sylow.eq_bot_of_one

added theorem Sylow.eq_top_of_zero

added def Sylow.equivProdPrimeFactors