mathlib

mathlib copied to clipboard

---

• [x] depends on: #13908
• [x] depends on: #13905
• [x] depends on: #13882
• [ ] depends on: #13933
• [x] depends on: #13934
• [x] depends on: #13961
• [ ] depends on: #14023

This PR/issue depends on:

• ~~leanprover-community/mathlib#13908~~
• ~~leanprover-community/mathlib#13905~~
• ~~leanprover-community/mathlib#13882~~
• ~~leanprover-community/mathlib#13933~~
• ~~leanprover-community/mathlib#13934~~
• ~~leanprover-community/mathlib#13961~~
• leanprover-community/mathlib#14023 By Dependent Issues (🤖). Happy coding!

This PR/issue depends on:

• ~~leanprover-community/mathlib#13908~~
• ~~leanprover-community/mathlib#13905~~
• ~~leanprover-community/mathlib#13882~~
• ~~leanprover-community/mathlib#13933~~
• ~~leanprover-community/mathlib#13934~~
• ~~leanprover-community/mathlib#13961~~
• ~~leanprover-community/mathlib#14023~~ By Dependent Issues (🤖). Happy coding!

Scott, what do you want to do with this? It is marked as ready for review, but I've gathered it is incomplete.

Do you want to have it in mathlib so that other people can build on it, or do you want to keep it somewhere else during the port, or something else again?

My preference is to have it in mathlib so others could potentially build on it. I'm unlikely to do any more in the near future.

Nice, I'm happy to see documentation like this.

Is the documentation being build as part of CI? It would be a shame if there was drift.

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