Commit 2024-10-16 21:14 f4d8a98e
View on Github →chore: copy Finsupp.smul_single' to (Add)MonoidAlgebra to avoid defeq abuse (#17825)
This seems to stem from Lean 3 where it was okay to simp with Finsupp lemmas in its type synonyms MonoidAlgebra and AddMonoidAlgebra. The discrimination tree in Lean 4 correctly catches the mismatch. So we copy the lemma to the type synonyms and remove some porting notes.