Def DirectSum.sigmaLcurry

Modification history

2024-10-14 12:17

Mathlib/Algebra/DirectSum/Module.lean

chore: unused arguments (#17348)

Modified DirectSum.sigmaLcurry View on Github →

2023-08-10 10:11

Mathlib/Algebra/DirectSum/Module.lean

feat: make `Dfinsupp.sigmaCurry` computable (#1947) …

Added DirectSum.sigmaLcurry View on Github →