Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-26 20:52 946454a8

View on Github →

feat(data/nat/factorization): various theorems on factorization and division (#11663)

Estimated changes

Modified src/data/nat/factorization.lean

added theorem nat.div_factorization_eq_tsub_of_dvd

added theorem nat.dvd_iff_div_factorization_eq_tsub

added theorem nat.dvd_iff_prime_pow_dvd_dvd

added theorem nat.exists_factorization_lt_of_lt

added theorem nat.factorization_eq_zero_of_non_prime

added theorem nat.pow_factorization_dvd

added theorem nat.prime_pow_dvd_iff_le_factorization