mathlib
f2db6a8f
- chore(algebra/order): enable dot syntax (#3643)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
chore(algebra/order): enable dot syntax (#3643) Add dot syntax aliases to some lemmas about order (e.g., `has_le.le.trans`). Also remove `lt_of_le_of_ne'` (was equivalent to `lt_of_le_of_ne`).
Author
urkud
Parents
6394e4d4
Loading