Theorem Finsupp.sum_comapDomain

Modification history

2026-09-09 15:18
Mathlib/Data/Finsupp/Basic.lean
feat(Data/Finsupp): support of `mapDomain` is image of support if nonneg (#43610) …
Deleted Finsupp.sum_comapDomainView on Github →
2023-02-01 05:31
Mathlib/Data/Finsupp/Basic.lean
feat: port Data.Finsupp.Basic (#1949) …
Added Finsupp.sum_comapDomainView on Github →