Commit 2023-02-27 13:48 19b42dda

View on Github →

feat: port Algebra.Order.Hom.Ring (#1482) Worked around https://github.com/leanprover-community/mathlib4/issues/2505, but finally everything works.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Hom/Ring.lean

added theorem OrderRingHom.cancel_left

added theorem OrderRingHom.cancel_right

added theorem OrderRingHom.coe_OrderAddMonoidHom_id

added theorem OrderRingHom.coe_OrderMonoidWithZeroHom_id

added theorem OrderRingHom.coe_RingHom_id

added theorem OrderRingHom.coe_coe_orderAddMonoidHom

added theorem OrderRingHom.coe_coe_orderMonoidWithZeroHom

added theorem OrderRingHom.coe_coe_ringHom

added theorem OrderRingHom.coe_comp

added theorem OrderRingHom.coe_copy

added theorem OrderRingHom.coe_id

added theorem OrderRingHom.coe_orderAddMonoidHom_apply

added theorem OrderRingHom.coe_orderMonoidWithZeroHom_apply

added theorem OrderRingHom.coe_ringHom_apply

added theorem OrderRingHom.comp_apply

added theorem OrderRingHom.comp_assoc

added theorem OrderRingHom.comp_id

added theorem OrderRingHom.copy_eq

added theorem OrderRingHom.ext

added theorem OrderRingHom.id_apply

added theorem OrderRingHom.id_comp

added theorem OrderRingHom.toFun_eq_coe

added def OrderRingHom.toOrderAddMonoidHom

added theorem OrderRingHom.toOrderAddMonoidHom_eq_coe

added def OrderRingHom.toOrderMonoidWithZeroHom

added theorem OrderRingHom.toOrderMonoidWithZeroHom_eq_coe

added theorem OrderRingHom.toRingHom_eq_coe

added structure OrderRingHom

added def OrderRingHomClass.toOrderRingHom

added def OrderRingIso.Simps.symmApply

added theorem OrderRingIso.coe_mk

added theorem OrderRingIso.coe_orderIso_refl

added theorem OrderRingIso.coe_ringEquiv_refl

added theorem OrderRingIso.coe_toOrderIso

added theorem OrderRingIso.coe_toOrderRingHom

added theorem OrderRingIso.coe_toOrderRingHom_refl

added theorem OrderRingIso.coe_toRingEquiv

added theorem OrderRingIso.ext

added theorem OrderRingIso.mk_coe

added theorem OrderRingIso.refl_apply

added theorem OrderRingIso.self_trans_symm

added theorem OrderRingIso.symm_bijective

added theorem OrderRingIso.symm_symm

added theorem OrderRingIso.symm_trans_self

added theorem OrderRingIso.toFun_eq_coe

added def OrderRingIso.toOrderIso

added theorem OrderRingIso.toOrderIso_eq_coe

added def OrderRingIso.toOrderRingHom

added theorem OrderRingIso.toOrderRingHom_eq_coe

added theorem OrderRingIso.toOrderRingHom_injective

added theorem OrderRingIso.toRingEquiv_eq_coe

added theorem OrderRingIso.trans_apply

added theorem OrderRingIso.trans_toRingEquiv

added theorem OrderRingIso.trans_toRingEquiv_aux

added structure OrderRingIso

added def OrderRingIsoClass.toOrderRingIso