Commit 2025-12-01 20:13 9eeaf70d

View on Github →

feat: Finsupp.sum in opposite monoid (#32253)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Finsupp/Basic.lean

added theorem AddOpposite.op_finsuppProd

added theorem AddOpposite.unop_finsuppProd

added theorem MulOpposite.op_finsuppSum

added theorem MulOpposite.unop_finsuppSum

Modified Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean

added theorem Finset.op_prod

modified theorem Finset.op_sum

added theorem Finset.unop_prod

modified theorem Finset.unop_sum