mathlib3

refactor(number_theory/divisors): redefine nat.divisors as a monoid hom

#16917

Open