Commit 2022-03-08 17:53 b4572d16

View on Github →

feat(algebra/order/hom/ring): Ordered ring isomorphisms (#12158) Define order_ring_iso, the type of ordered ring isomorphisms, along with its typeclass order_ring_iso_class.

Estimated changes

Modified src/algebra/order/hom/ring.lean

modified structure order_ring_hom

added theorem order_ring_iso.coe_mk

added theorem order_ring_iso.coe_order_iso_refl

added theorem order_ring_iso.coe_ring_equiv_refl

added theorem order_ring_iso.coe_to_order_iso

added theorem order_ring_iso.coe_to_order_ring_hom

added theorem order_ring_iso.coe_to_order_ring_hom_refl

added theorem order_ring_iso.coe_to_ring_equiv

added theorem order_ring_iso.ext

added theorem order_ring_iso.mk_coe

added theorem order_ring_iso.refl_apply

added theorem order_ring_iso.self_trans_symm

added def order_ring_iso.simps.symm_apply

added theorem order_ring_iso.symm_symm

added theorem order_ring_iso.symm_trans_self

added theorem order_ring_iso.to_fun_eq_coe

added def order_ring_iso.to_order_iso

added theorem order_ring_iso.to_order_iso_eq_coe

added def order_ring_iso.to_order_ring_hom

added theorem order_ring_iso.to_order_ring_hom_eq_coe

added theorem order_ring_iso.to_ring_equiv_eq_coe

added theorem order_ring_iso.trans_apply

added structure order_ring_iso

Modified src/order/hom/basic.lean

added theorem le_map_inv_iff

added theorem lt_map_inv_iff

added theorem map_inv_le_iff

added theorem map_inv_lt_iff

added theorem map_lt_map_iff