Main definitions #
- "identity" maps between
- stronger versions of
The defining features of these operations is that they preserve the function and support:
as well as preserving arithmetic operations.
For the bundled equivalences, we provide lemmas that they reduce to
Implementation notes #
finsuppEquivDFinsupp computably by adding
[DecidableEq ι] and
[Π m : M, Decidable (m ≠ 0)] arguments. To aid with definitional unfolding,
these arguments are also present on the
Basic definitions and lemmas #
Note that the elaborator has a lot of trouble with this definition - it is often necessary to
(DFinsupp.toFinsupp f : ι →₀ M) instead of
f.toFinsupp, as for some unknown reason
using dot notation or omitting the type ascription prevents the type being resolved correctly.