[Merged by Bors] - feat: define prodPrimeFactors as an ArithmeticFunction

[FLDutchmann]

Define the arithmetic function $n \mapsto \prod_{p \mid n} f(p)$. This PR further proves that it's multiplicative and relates it to Dirichlet convolution. Finally it proves two identities that can be applied in a context where you're not working exclusively with ArithmeticFunctions

This construction was mentioned on zulip

---

prodToFinsetFactors_add_of_squarefree uses Nat division, as discussed earlier in #6344. To summarise why I think it is helpful:
On the LHS we have a product over the distinct factors of n, which is expanded to a product over the subsets of factors n.
On the RHS we have Dirichlet convolution. The natural thing to try is to write it as a sum over divisorsAntidiagonal, but relating that to subsets of factors n is difficult. Instead I write it as a sum over divisors, introducing Nat division, so that I can apply the existing (nontrivial!) theorem Nat.sum_divisors_filter_squarefree, which perfectly lines up the sums along the powerset.

Avoiding Nat division here would mean re-proving Nat.sum_divisors_filter_squarefree for divisorsAntidiagonal (likely only for squarefree n, since you can't filter by Squarefree). I claim it's easier to have a six-line lemma about Nat division instead.

[eric-wieser]

This looks like a mis-use of NeZero to me

[FLDutchmann]

I chose to do this based on a suggestion by @kbuzzard, and it does come in handy for IsMultiplicative.prodToFinsetFactors in that (a) it works with simp_rw and (b) it automatically deduces NeZero (x*y)

[alreadydone]

Define the arithmetic function $n \mapsto \prod_{p \mid n} f(p)$.

For f = id this is the radical of n and can be used to state the abc conjecture, now that we have #6508 ... How easy is the equivalence with Szpiro's conjecture?

Zulip

[b-mehta]

I'm not sure this notation is a good idea - it could also refer to the product over primes (rather than prime divisors of a fixed number)

[FLDutchmann]

That's a fair concern. It was only used in one place so I've removed it.

It does make me think about other possible notations for the bare arithmetic function. Something like ∏ᵖ p ∣ _, f p or ∏ᵖ p ∣ ·, f p comes to mind but they obviously interfere with much more fundamental notation.

[jcommelin]

ToFinsetFactors occurs in a lot of places. I think that's a sign that we should define the prime divisors of a number as a finset, and give it a name. Could be factorsSet or factors'. Or maybe we have a quick poll on zulip about a good name.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style