mathlib

mathlib copied to clipboard

We add some documentation, and golf slightly by marking nat.elim and nat.cases as reducible.

---

I'm not sure if it's a good idea to mark new things as reducible, especially if the only benefit is some golf - sometimes reducible is regarded as code smell; so I'm very hesitant about this change being in a chore nolint PR.

No idea what I was thinking with the reducible tags, they've been reverted.

Thanks!

bors merge

Pull request successfully merged into master.

Build succeeded:

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