mathlib
d7da6980
- feat(data/set/basic): add `set.subsingleton_range` (#17248)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
feat(data/set/basic): add `set.subsingleton_range` (#17248) Also use it to golf a proof.
Author
urkud
Parents
00d450eb
Loading