Commit 2025-05-12 20:50 5f30136d

View on Github →

refactor(Finsupp): redefine curry and uncurry (#24746) The new versions have definitional equalities that match Function.curry and Function.uncurry. This also makes these computable, at the expense of an extra DecidableEq argument.

Estimated changes

Modified Mathlib/Data/Finsupp/Basic.lean

modified theorem Finsupp.curry_apply

modified theorem Finsupp.sum_curry_index

added theorem Finsupp.sum_uncurry_index'

added theorem Finsupp.sum_uncurry_index

modified theorem Finsupp.support_curry

Modified Mathlib/LinearAlgebra/Finsupp/Defs.lean

modified theorem Finsupp.finsuppProdLEquiv_symm_apply_apply

Modified Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean

modified theorem Finsupp.linearCombination_smul

Modified Mathlib/RingTheory/AlgebraTower.lean

Modified Mathlib/RingTheory/Norm/Transitivity.lean

Modified Mathlib/RingTheory/Unramified/Finite.lean