Theorem Finsupp.mapDomain_apply_of_injective

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) …
Added Finsupp.mapDomain_apply_of_injectiveView on Github →