Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-26 11:53 7f0f3f19

View on Github →

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.

Estimated changes

added structure order_add_monoid_hom
added theorem order_monoid_hom.ext
added structure order_monoid_hom