Commit 2022-05-12 18:30 27e7f7ac

View on Github →

feat(number_theory/divisors): add filter_dvd_eq_proper_divisors (#14049) Adds filter_dvd_eq_proper_divisors and golfs filter_dvd_eq_divisors and a few other lemmas

Estimated changes

Modified src/number_theory/divisors.lean

modified theorem nat.filter_dvd_eq_divisors

added theorem nat.filter_dvd_eq_proper_divisors

modified theorem nat.mem_divisors