mathlib3

7b6c4072 - feat(number_theory/divisors): add `prod_div_divisors` and `sum_div_divisors` (#12087)

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`)