mathlib3

7f0f3f19 - feat(algebra/order/hom/monoid): Ordered monoid/group homomorphisms (#11633)

feat(algebra/order/hom/monoid): Ordered monoid/group homomorphisms (#11633) Define * `order_add_monoid_hom` with notation `→+o` * `order_monoid_hom` with notation `→*o` * `order_monoid_with_zero_hom` with notation `→*₀o` and their corresponding hom classes. Also add a few missing API lemmas in `algebra.group.hom` and `order.hom.basic`.