mathlib

mathlib copied to clipboard

This splits data.set.pointwise and data.finset.pointwise each into several smaller files.

This allows us to remove or defer some imports, e.g. of order.well_founded_set and of algebra.big_operators.basic.

No changes to statements of theorems, just relocating.

---

I understand moving the later instances, but why move has_smul?

To remove the dependence on algebra.module.basic and algebra.big_operators.basic.

has_smul.smul is in algebra.group.defs

Okay, I agree the smul instance shouldn't have been moved out. I'll reconsider, but maybe not immediately. :-)

@YaelDillies, I've restored the material on smul to its rightful place.

Thanks!

Given this branch is a week behind master I suggest merging master before sending it to bors.

bors d+

:v: semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests