Commit 2023-08-10 10:11 8c390f68

View on Github →

feat: make Dfinsupp.sigmaCurry computable (#1947) ~~mathlib3 PR: https://github.com/leanprover-community/mathlib/pull/18316~~

Estimated changes

Modified Mathlib/Algebra/DirectSum/Basic.lean

added def DirectSum.sigmaCurry

added def DirectSum.sigmaCurryEquiv

Modified Mathlib/Algebra/DirectSum/Module.lean

added def DirectSum.sigmaLcurry

added def DirectSum.sigmaLcurryEquiv

Modified Mathlib/Data/DFinsupp/Basic.lean

added def DFinsupp.sigmaCurry

added def DFinsupp.sigmaCurryEquiv

modified theorem DFinsupp.sigmaCurry_add

modified theorem DFinsupp.sigmaCurry_apply

modified theorem DFinsupp.sigmaCurry_zero