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.

Estimated changes