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

[b-mehta]

nat.divisors unconditionally preserves multiplication, so this bundles it as a monoid hom, similar for nat.divisors_antidiagonal.

This PR also changes nat.divisors to be defined in terms of nat.divisors_antidiagonal, which drastically simplifies some later proofs

---

• [ ] depends on: #16935
• [x] depends on: #16936

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#16935~~
• ~~leanprover-community/mathlib#16936~~ By Dependent Issues (🤖). Happy coding!

[b-mehta]

Yeah I'm happy with that, as long as my current definition is there as a lemma instead

On Sun, 30 Oct 2022, 15:28 Eric Wieser, @.***> wrote:

@.**** commented on this pull request.

In src/number_theory/divisors.lean https://github.com/leanprover-community/mathlib/pull/16917#discussion_r1008883421 :

/-- divisors n is the finset of divisors of n. As a special case, divisors 0 = ∅. -/

-def divisors : finset ℕ := finset.filter (λ x : ℕ, x ∣ n) (finset.Ico 1 (n + 1))

+def divisors : ℕ →* finset ℕ := (monoid_hom.fst ℕ ℕ).image.comp divisors_antidiagonal

Can we compromise on defining divisors_antidiagonal in term of divisors and not the other way around? Either as

n.divisors.map ⟨λ d, (d, n/d), λ p₁ p₂, congr_arg prod.fst⟩ = n.divisors_antidiagonal

or

n.divisors.map ⟨λ d, (n/d, d), λ p₁ p₂, congr_arg prod.snd⟩ = n.divisors_antidiagonal

— Reply to this email directly, view it on GitHub https://github.com/leanprover-community/mathlib/pull/16917#discussion_r1008883421, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHESIORCFBJPSOHLN6VOCZTWF2AZ3ANCNFSM6AAAAAARCTC5GU . You are receiving this because you authored the thread.Message ID: @.***>