mathlib3
refactor(data/dfinsupp/basic): move material on `dfinsupp.sum` and `dfinsupp.prod` to new file
#16174
Open

refactor(data/dfinsupp/basic): move material on `dfinsupp.sum` and `dfinsupp.prod` to new file #16174

stuart-presnell wants to merge 6 commits into master from SP_dfinsupp_refactor
stuart-presnell
stuart-presnell Move up section `map_range`
630b7336
stuart-presnell Move sum and prod to new file
1e4b3503
stuart-presnell stuart-presnell added awaiting-review
stuart-presnell Fix long line
08ac68ec
stuart-presnell Fix imports
570dbb9f
stuart-presnell Trim imports
9ea1c78d
stuart-presnell Fix import
a8422536
Vierkantor
Vierkantor commented on 2022-10-05
Vierkantor Vierkantor removed awaiting-review
Vierkantor Vierkantor added awaiting-author
Vierkantor Vierkantor assigned Vierkantor Vierkantor 3 years ago
stuart-presnell
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
Labels
Milestone