mathlib
146d3d1f
- chore(*/..eq): add is_refl instances (#15963)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(*/..eq): add is_refl instances (#15963) This allows the use of docs#of_eq, an extremely underused utility method. Also fixes `smodeq` to match the `rfl/refl` conventions.
Author
ericrbg
Parents
cad35c79
Loading