Theorem AddMonoidAlgebra.smul_single'

Modification history

2024-10-16 21:14

Mathlib/Algebra/MonoidAlgebra/Defs.lean

chore: copy `Finsupp.smul_single'` to (`Add`)`MonoidAlgebra` to avoid defeq abuse (#17825) …

Added AddMonoidAlgebra.smul_single'View on Github →