feat(NumberTheory/SmoothNumbers): multiplicativity

[rwst]

trafficstars

Prove that the product of two n-smooth numbers is an n-smooth number. Uses two helper lemmas.

---

[rwst]

Thanks for the improvements. I'm learning.

[rwst]

Here it is!

[Rida-Hamadani]

LGTM

[grunweg]

It's great to see the informal reviewing process that already happened, thanks a lot! In order for this PR to be merged, somebody with review powers still needs to give explicit approval. Let me label this PR with awaiting-review so it shows up in the "review queue" where it will be noticed.

[grunweg]

awaiting-author

[rwst]

I would like to deal with the comments in a sequential way, not the least in order to preserve the optimization steps that were done.

[rwst]

@MichaelStollBayreuth I have flagged the PR as WIP, to signal that there is an alternative (and mathematically cleaner) way to do this. I will now open a new branch for that work. Once that is done and merged, this one should be closed.

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by loefflerd.

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style