Commit 2025-11-14 09:22 87f042f7

View on Github →

chore(Finsupp): move mapRange.equiv earlier (#31324) Move mapRange.equiv to Data.Finsupp.Defs and mapRange.addEquiv to Algebra.Group.Finsupp. This lets us not import fields when defining finsuppAntidiag. As previously, I am basing myself off the idea that Finsupp will at some point in the future be generalised to other base points (rather than just 0 as it is now), and that therefore anything under Data.Finsupp should not be algebraic (apart from mentioning 0).

Estimated changes

modified theorem Finsupp.mapRange_comp
modified theorem Finsupp.mapRange_mapRange
modified theorem Finsupp.support_zipWith
modified def Finsupp.zipWith
modified theorem Finsupp.zipWith_apply