Theorem Finsupp.mem_vaddAntidiagonal_of_addGroup

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.mem_vaddAntidiagonal_of_addGroupView 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.mem_vaddAntidiagonal_of_addGroupView on Github →