Theorem MulOpposite.op_finsuppSum

Modification history

2025-12-08 14:29
Mathlib/Algebra/BigOperators/Finsupp/Basic.lean
chore: additivise `MulOpposite.op_finsuppSum` to itself (#32501) …
Modified MulOpposite.op_finsuppSumView on Github →
2025-12-01 20:13
Mathlib/Algebra/BigOperators/Finsupp/Basic.lean
feat: `Finsupp.sum` in opposite monoid (#32253)
Added MulOpposite.op_finsuppSumView on Github →