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.
feat: delaborators for Finset.prod and Finset.sum (#3772)
Also fixes some spacing in their syntax commands, which impacts pretty printing.