Commit 2026-01-19 08:37 85cb0df0

View on Github →

refactor(Data/Finsupp): remove DecidableEq argument from curry (#33490) This is motivated by it spuriously requiring extra decidability assumptions in group cohomology. This partially reverts #24746. No motivation was given there for why computability was necessary. Finsupp.curry will be made computable again anyway once Finsupp is redefined to be DFinsupp. From ClassFieldTheory

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

Modified Mathlib/Algebra/MonoidAlgebra/Defs.lean

Modified Mathlib/Algebra/MonoidAlgebra/MapDomain.lean

Modified Mathlib/Data/Finsupp/Basic.lean

modified theorem Finsupp.support_curry

Modified Mathlib/LinearAlgebra/Finsupp/Defs.lean

Modified Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean

modified theorem Finsupp.linearCombination_smul

Modified Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean

modified def groupCohomology.inhomogeneousCochainsIso

modified def groupCohomologyIso

modified def groupCohomologyIsoExt

Modified Mathlib/RepresentationTheory/Homological/GroupCohomology/FiniteCyclic.lean

Modified Mathlib/RepresentationTheory/Homological/GroupCohomology/Shapiro.lean

Modified Mathlib/RepresentationTheory/Homological/Resolution.lean

Modified Mathlib/RepresentationTheory/Rep.lean

Modified Mathlib/RingTheory/AlgebraTower.lean