Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-10 10:46 6afaf36d

View on Github →

feat(algebra/order/hom/ring): Ordered semiring/ring homomorphisms (#11634) Define order_ring_hom with notation →+*o along with its hom class.

Estimated changes

modified structure order_add_monoid_hom
modified structure order_monoid_hom
modified structure order_monoid_with_zero_hom
added theorem order_ring_hom.coe_id
added theorem order_ring_hom.comp_id
added theorem order_ring_hom.ext
added theorem order_ring_hom.id_comp
added structure order_ring_hom
added def ring_hom.copy