Commit 2025-07-03 14:11 5beabdc1

View on Github →

feat: Finsupp.supportedEquivFinsupp_symm_single (#26314)

Estimated changes

Modified Mathlib/Data/Finsupp/Basic.lean

modified def Finsupp.restrictSupportEquiv

added theorem Finsupp.restrictSupportEquiv_symm_apply_coe

added theorem Finsupp.restrictSupportEquiv_symm_single

Modified Mathlib/LinearAlgebra/Finsupp/Supported.lean

added theorem Finsupp.supportedEquivFinsupp_symm_single