Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-01-05 14:15
3bd2044b
View on Github →
chore(data/nat/prime): reuse a result from algebra.big_operators.associated (
#11143
)
Estimated changes
Modified
src/algebra/big_operators/associated.lean
deleted
theorem
nat.prime.dvd_finset_prod_iff
deleted
theorem
nat.prime.dvd_finsupp_prod_iff
deleted
theorem
prime.dvd_prod_iff
Created
src/data/list/prime.lean
added
theorem
mem_list_primes_of_dvd_prod
added
theorem
perm_of_prod_eq_prod
added
theorem
prime.dvd_prod_iff
added
theorem
prime.not_dvd_prod
added
theorem
prime_dvd_prime_iff_eq
Modified
src/data/nat/prime.lean
deleted
theorem
nat.mem_list_primes_of_dvd_prod
deleted
theorem
nat.perm_of_prod_eq_prod
deleted
theorem
nat.prime.dvd_prod_iff
deleted
theorem
nat.prime.not_dvd_prod