Theorem MonoidAlgebra.smul_single'

Modification history

2025-08-13 12:33

Mathlib/Algebra/MonoidAlgebra/Defs.lean

chore(Algebra/MonoidAlgebra): split Defs.lean further (#28030) …

Modified MonoidAlgebra.smul_single'View on Github →

2024-10-16 21:14

Mathlib/Algebra/MonoidAlgebra/Defs.lean

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

Added MonoidAlgebra.smul_single'View on Github →