[Merged by Bors] - refactor(Algebra/Polynomial/Basic): define nsmul/zsmul for Polynomial

[Vierkantor]

The goal of this PR is to make the ring instances on Polynomial independent of the module structure. This is currently somewhat useless and will only be useful in an upcoming PR that splits this entire file Polynomial/Basic.lean. But since adding definitions while splitting files is very annoying to review, let's do it in multiple steps.

---

[github-actions]

PR summary 4318efebfe

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ instNSMul
+ instZSMul
+ ofFinsupp_nsmul
+ ofFinsupp_zsmul
+ toFinsupp_nsmul
+ toFinsupp_zsmul

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Ruben-VandeVelde]

Thanks!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

[adomani]

Thanks!

bors merge

[eric-wieser]

The goal of this PR is to make the ring instances on Polynomial independent of the module structure.

Why is this desirable? The nsmul/zsmul pattern is a lot more pleasant if you can define the general smul instance first and recover the nsmul/zsmul actions as special cases.

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build

[Vierkantor]

Ouch, the bot was slightly too fast for your review :(

Anyway, the nsmul/zsmul instance are defined separately since there is no correct instance of SMul M R -> SMul M R[X]: they need to preserve 0 too.

[eric-wieser]

Right; I guess my claim is that SMulZeroClass should be treated as just as primitive as MulZeroClass, and so it doesn't seem problematic to me to require it when building the AddCommGroup structure.

[adomani]

Oh, the second PR that I merged and I already did something controversial... 🤦