mathlib3

feat(number_theory/divisors): add divisors_mul

#17041

Open