Theorem Finsupp.mapRange_surjective

Modification history

2024-10-11 09:39
Mathlib/Data/Finsupp/Defs.lean
feat: `Finsupp.mapRange` of a surjective function is surjective (#17637) …
Added Finsupp.mapRange_surjectiveView on Github →