Commit 2026-03-15 13:15 815dd043

View on Github →

feat(Data/Finsupp): more API for sumElim (#36675) For this, also make mapDomain_apply simp.

Estimated changes

Modified Mathlib/Data/Finsupp/Basic.lean

modified theorem Finsupp.coe_sumElim

modified theorem Finsupp.mapDomain_apply

added theorem Finsupp.mapDomain_swap_sumElim

modified def Finsupp.sumElim

modified theorem Finsupp.sumElim_apply

added theorem Finsupp.sumElim_eq_add

modified theorem Finsupp.sumElim_inl

modified theorem Finsupp.sumElim_inr

added theorem Finsupp.sumElim_single_single

added theorem Finsupp.sumElim_single_zero

added theorem Finsupp.sumElim_zero_single

added theorem Finsupp.sumElim_zero_zero