Theorem Finsupp.smul_eq

Modification history

2026-04-28 01:10
Mathlib/Data/Finsupp/PointwiseSMul.lean
refactor(Algebra/MonoidAlgebra/PointwiseSMul): switch action from Finsupp to (Add)MonoidAlgebra and multiplicativize (#35243) …
Deleted Finsupp.smul_eqView on Github →
2025-10-30 14:15
Mathlib/Data/Finsupp/PointwiseSMul.lean
feat (Data/Finsupp): define convolution smul for finsupps on formal functions (#28819) …
Added Finsupp.smul_eqView on Github →