Commit 2024-11-15 22:23 0b854502

refactor(Algebra/Polynomial/Basic): define nsmul/zsmul for Polynomial (#19095) 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.