[Merged by Bors] - feat(Data/Finset/NatDivisors): Nat.divisors of a product

[adomani]

The function Nat.divisors as a multiplicative homomorphism ℕ →* Finset ℕ.

This result is in a new file Data/Finset/NatDivisors, to avoid adding imports and/or lengthening existing files.

---

[urkud]

I golfed your proof. I'm not sure that you need more imports for the new proof. Also, you can get a slightly different version of Nat.Prime.divisors_sq like this:

lemma Prime.divisors_sq {p : ℕ} (hp : p.Prime) : (p ^ 2).divisors = {p ^ 2, p, 1} := by
  simp [divisors_prime_pow hp, range_succ]

I'm not sure that we have a nice way to reorder a chain of inserts.

Also, I think that it would be nice to have a version for Finset.prod of numbers (and possibly for List.prod and/or Multiset.prod as well).

[adomani]

Yuri, I added the Multiset and the List version. I have to go now, but I'll look into the Finset version and whether this fits better in an earlier file later!

Thanks!

[adomani]

Yuri, I added the Finset lemmas, but either I took a wrong turn, or there was some missing API around Pointwise.

Anyway, I could still not move the lemmas in a different file, since I could not find any interaction between Nat.divisors and Pointwise: either a file develops the theory of Nat.divisors and has no Pointwise, or there is Pointwise, but no Nat.divisors.

From this point of view, it may make sense to create this new file, what do you think?

[adomani]

Yuri, your latest commit is such an improvement over my butchering of the lemmas! Thanks!

[urkud]

Thanks! 🎉
bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Check all files imported