mathlib

7767ef8b - feat(number_theory/divisors): defines the finsets of divisors/proper divisors, perfect numbers, etc. (#4310)

feat(number_theory/divisors): defines the finsets of divisors/proper divisors, perfect numbers, etc. (#4310) Defines `nat.divisors n` to be the set of divisors of `n`, and `nat.proper_divisors` to be the set of divisors of `n` other than `n`. Defines `nat.divisors_antidiagonal` in analogy to other `antidiagonal`s used to define convolutions Defines `nat.perfect`, the predicate for perfect numbers Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>