mathlib
5027b283
- move(data/nat/choose/bounds): Move from `combinatorics.choose.bounds` (#12051)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
move(data/nat/choose/bounds): Move from `combinatorics.choose.bounds` (#12051) This file fits better with all other files about `nat.choose`. My bad for originally proposing it goes alone under `combinatorics`.
Author
YaelDillies
Parents
52aaf173
Loading