Def DirectSum.sigmaLcurry

Modification history

2023-08-10 10:11
Mathlib/Algebra/DirectSum/Module.lean
feat: make `Dfinsupp.sigmaCurry` computable (#1947) …
Added DirectSum.sigmaLcurryView on Github →