Commit 2024-12-10 21:48 75368bee
View on Github →chore(Data/Finsupp): split off basic scalar multiplication (#19205)
In the comments of #19095 we discussed that MonoidAlgebra and Polynomial need scalar multiplication by Nat or Int early on, to define a Semiring or Ring structure. We can define a generic SMulWithZero instance and then specialize it to get nsmul and zsmul, but only if that instance is available early on for Finsupp. So: split this off from Finsupp/Basic.lean into a higher-up file.
This PR used Damiano's upstreamableDecls linter to find out which results could move together with the definitions for free.