mathlib3
1a7fb7e4
- feat(data/list/sort): add sorted.rel_of_mem_take_of_mem_drop (#6027)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
feat(data/list/sort): add sorted.rel_of_mem_take_of_mem_drop (#6027) Also renames the existing lemmas to enable dot notation Co-authored-by: pechersky@users.noreply.github.com
Author
eric-wieser
Parents
b98b5f6b
Loading