mathlib3

c66f2aee - feat(number_theory/divisors): more thoroughly link `divisors_antidiagonal` and `divisors` (#17050)

feat(number_theory/divisors): more thoroughly link `divisors_antidiagonal` and `divisors` (#17050) The lemmas in this file seemed to jump to proving statements about products over sets rather than first proving equalities of the sets themselves. This adds those skipped lemmas (from scratch) and golfs the derived results. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>