Commit 2026-05-23 12:03 504fc865

View on Github →

feat: add congruence lemmas for (d)finsupp big operators (#39422) Also adds the missing n-ary product lemmas to match the existing sum lemmas.

Estimated changes

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

added theorem Finsupp.prod_congr_of_eq_on_union

Modified Mathlib/Data/DFinsupp/BigOperators.lean

added theorem DFinsupp.prod_congr_of_eq_on_union

added theorem DFinsupp.prod_of_support_subset

Modified Mathlib/GroupTheory/Congruence/BigOperators.lean

Modified Mathlib/RingTheory/Congruence/BigOperators.lean

Modified Mathlib/RingTheory/TwoSidedIdeal/BigOperators.lean

added theorem TwoSidedIdeal.dfinsuppProd_mem

added theorem TwoSidedIdeal.dfinsuppSum_mem

added theorem TwoSidedIdeal.finsuppProd_mem

added theorem TwoSidedIdeal.finsuppSum_mem