Commit 2025-07-13 20:41 d2064d62

View on Github →

feat: AddEquiv.finsuppUnique_apply (#27045) ... and some other easy lemmas From Toric

Estimated changes

Modified Mathlib/Algebra/FreeAbelianGroup/Finsupp.lean

added theorem Finsupp.toFreeAbelianGroup_single

modified theorem FreeAbelianGroup.toFinsupp_of

Modified Mathlib/Algebra/Group/Finsupp.lean

added theorem AddEquiv.finsuppUnique_apply