Commit 2022-02-18 19:52 7b6c4072
View on Github →feat(number_theory/divisors): add prod_div_divisors and sum_div_divisors (#12087)
Adds lemma prod_div_divisors : ∏ d in n.divisors, f (n/d) = n.divisors.prod f and sum_div_divisors.
Also proves image_div_divisors_eq_divisors : image (λ (x : ℕ), n / x) n.divisors = n.divisors
and div_eq_iff_eq_of_dvd_dvd : n / x = n / y ↔ x = y (where n ≠ 0 and x ∣ n and y ∣ n)