Def Finsupp.mapDomain

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) …

Modified Finsupp.mapDomain View on Github →

2023-02-01 05:31

Mathlib/Data/Finsupp/Basic.lean

feat: port Data.Finsupp.Basic (#1949) …

Added Finsupp.mapDomain View on Github →