mathlib3
6df3143a
- chore(combinatorics/choose/bounds): move to nat namespace (#10106)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
chore(combinatorics/choose/bounds): move to nat namespace (#10106) There are module docstrings elsewhere that expect this to be in the `nat` namespace with the other `choose` lemmas.
Author
eric-wieser
Parents
0dcb1849
Loading