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