mathlib
324a605f
- chore(order): rename `preorder_hom` to `order_hom` (#10750)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
chore(order): rename `preorder_hom` to `order_hom` (#10750) For consistency with `order_embedding` and `order_iso`, this PR renames `preorder_hom` to `order_hom`, at the request of @YaelDillies.
Author
Vierkantor
Parents
35cd7c0c
Loading