Commit 2023-05-03 23:01 093dc264

View on Github →

feat: delaborators for Finset.prod and Finset.sum (#3772) Also fixes some spacing in their syntax commands, which impacts pretty printing.

Estimated changes