mathlib
ef377a92
- chore(data/list/sort): docs, add a few lemmas (#5274)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
chore(data/list/sort): docs, add a few lemmas (#5274) * Add a module docstring and section headers. * Rename `list.eq_of_sorted_of_perm` to `list.eq_of_perm_of_sorted`; the new name reflects the order of arguments. * Add a few lemmas.
Author
urkud
Parents
aec64b17
Loading