Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-06 07:25 24ebc5cd

View on Github →

feat(group_theory/sylow): the cardinality of a sylow group (#11776)

Estimated changes

Modified src/algebra/is_prime_pow.lean

Modified src/data/nat/factorization.lean

added theorem nat.prime.pow_dvd_iff_dvd_pow_factorization

added theorem nat.prime.pow_dvd_iff_le_factorization

deleted theorem nat.prime_pow_dvd_iff_le_factorization

Modified src/group_theory/sylow.lean

added theorem sylow.card_eq_multiplicity