Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nat.prime_pow_dvd_iff_le_factorization

Modification history

2022-02-06 07:25
src/data/nat/factorization.lean
feat(group_theory/sylow): the cardinality of a sylow group (#11776)
Deleted nat.prime_pow_dvd_iff_le_factorizationView on Github →
2022-01-26 20:52
src/data/nat/factorization.lean
feat(data/nat/factorization): various theorems on factorization and division (#11663)
Added nat.prime_pow_dvd_iff_le_factorizationView on Github →