Commit 2022-12-14 01:47 098452be

View on Github →

feat: port Algebra.Order.Hom.Monoid (#944) mathlib3 SHA: 3342d1b2178381196f818146ff79bc0e7ccd9e2d

depends on: #952

Estimated changes

Modified Mathlib.lean

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

added structure OrderAddMonoidHom

added theorem OrderMonoidHom.cancel_left

added theorem OrderMonoidHom.cancel_right

added theorem OrderMonoidHom.coe_comp

added theorem OrderMonoidHom.coe_comp_monoidHom

added theorem OrderMonoidHom.coe_comp_orderHom

added theorem OrderMonoidHom.coe_copy

added theorem OrderMonoidHom.coe_id

added theorem OrderMonoidHom.coe_mk

added theorem OrderMonoidHom.coe_monoidHom

added theorem OrderMonoidHom.coe_mul

added theorem OrderMonoidHom.coe_one

added theorem OrderMonoidHom.coe_orderHom

added def OrderMonoidHom.comp

added theorem OrderMonoidHom.comp_apply

added theorem OrderMonoidHom.comp_assoc

added theorem OrderMonoidHom.comp_id

added theorem OrderMonoidHom.comp_mul

added theorem OrderMonoidHom.comp_one

added theorem OrderMonoidHom.copy_eq

added theorem OrderMonoidHom.ext

added theorem OrderMonoidHom.id_comp

added def OrderMonoidHom.mk'

added theorem OrderMonoidHom.mk_coe

added theorem OrderMonoidHom.mul_apply

added theorem OrderMonoidHom.mul_comp

added theorem OrderMonoidHom.one_apply

added theorem OrderMonoidHom.one_comp

added theorem OrderMonoidHom.toFun_eq_coe

added theorem OrderMonoidHom.toMonoidHom_eq_coe

added theorem OrderMonoidHom.toMonoidHom_injective

added def OrderMonoidHom.toOrderHom

added theorem OrderMonoidHom.toOrderHom_eq_coe

added theorem OrderMonoidHom.toOrderHom_injective

added structure OrderMonoidHom

added theorem OrderMonoidWithZeroHom.cancel_left

added theorem OrderMonoidWithZeroHom.cancel_right

added theorem OrderMonoidWithZeroHom.coe_comp

added theorem OrderMonoidWithZeroHom.coe_comp_monoidWithZeroHom

added theorem OrderMonoidWithZeroHom.coe_comp_orderMonoidHom

added theorem OrderMonoidWithZeroHom.coe_copy

added theorem OrderMonoidWithZeroHom.coe_id

added theorem OrderMonoidWithZeroHom.coe_mk

added theorem OrderMonoidWithZeroHom.coe_monoidWithZeroHom

added theorem OrderMonoidWithZeroHom.coe_mul

added theorem OrderMonoidWithZeroHom.coe_orderMonoidHom

added def OrderMonoidWithZeroHom.comp

added theorem OrderMonoidWithZeroHom.comp_apply

added theorem OrderMonoidWithZeroHom.comp_assoc

added theorem OrderMonoidWithZeroHom.comp_id

added theorem OrderMonoidWithZeroHom.comp_mul

added theorem OrderMonoidWithZeroHom.copy_eq

added theorem OrderMonoidWithZeroHom.ext

added theorem OrderMonoidWithZeroHom.id_comp

added theorem OrderMonoidWithZeroHom.mk_coe

added theorem OrderMonoidWithZeroHom.mul_apply

added theorem OrderMonoidWithZeroHom.mul_comp

added theorem OrderMonoidWithZeroHom.toFun_eq_coe

added theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_eq_coe

added theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_injective

added def OrderMonoidWithZeroHom.toOrderMonoidHom

added theorem OrderMonoidWithZeroHom.toOrderMonoidHom_eq_coe

added theorem OrderMonoidWithZeroHom.toOrderMonoidHom_injective

added structure OrderMonoidWithZeroHom

added theorem antitone_iff_map_nonneg

added theorem antitone_iff_map_nonpos

added theorem map_nonneg

added theorem map_nonpos

added theorem monotone_iff_map_nonneg

added theorem monotone_iff_map_nonpos

added theorem strict_anti_iff_map_neg

added theorem strict_anti_iff_map_pos

added theorem strict_mono_iff_map_neg

added theorem strict_mono_iff_map_pos