Commit 2025-01-23 21:56 2a71f56e
View on Github →fix: add missing MonoidAlgebra.smul_single (#20933)
This eliminates some erws.
Also fixes bad generated simp lemmas about singleOneRingHom and singleZeroRingHom, which previously included unwanted toFun terms.