mathlib3
086469f7 - chore(order/*): Change `order_hom` notation (#10988)

Commit
4 years ago
chore(order/*): Change `order_hom` notation (#10988) This changes the notation for `order_hom` from `α →ₘ β` to `α →o β` to match `order_embedding` and `order_iso`, which are respectively `α ↪o β` and `α ≃o β`. This also solves the conflict with measurable functions.
Author
Parents
Loading