Commit 2025-07-23 21:12 0daba2d9

View on Github →

chore(Algebra/Order/Hom/Monoid): separate MonoidWithZero material into separate file (#27337) This PR moves material that uses MonoidWithZero into a separate file.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/GroupWithZero/Lex.lean

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

deleted def OrderMonoidIso.unitsWithZero

deleted def OrderMonoidIso.withZero

deleted def OrderMonoidIso.withZeroUnits

deleted theorem OrderMonoidWithZeroHom.cancel_left

deleted theorem OrderMonoidWithZeroHom.cancel_right

deleted theorem OrderMonoidWithZeroHom.coe_comp

deleted theorem OrderMonoidWithZeroHom.coe_comp_monoidWithZeroHom

deleted theorem OrderMonoidWithZeroHom.coe_comp_orderMonoidHom

deleted theorem OrderMonoidWithZeroHom.coe_copy

deleted theorem OrderMonoidWithZeroHom.coe_id

deleted theorem OrderMonoidWithZeroHom.coe_mk

deleted theorem OrderMonoidWithZeroHom.coe_monoidWithZeroHom

deleted theorem OrderMonoidWithZeroHom.coe_mul

deleted theorem OrderMonoidWithZeroHom.coe_orderMonoidHom

deleted def OrderMonoidWithZeroHom.comp

deleted theorem OrderMonoidWithZeroHom.comp_apply

deleted theorem OrderMonoidWithZeroHom.comp_assoc

deleted theorem OrderMonoidWithZeroHom.comp_id

deleted theorem OrderMonoidWithZeroHom.comp_mul

deleted theorem OrderMonoidWithZeroHom.copy_eq

deleted theorem OrderMonoidWithZeroHom.ext

deleted theorem OrderMonoidWithZeroHom.id_comp

deleted theorem OrderMonoidWithZeroHom.mk_coe

deleted theorem OrderMonoidWithZeroHom.mul_apply

deleted theorem OrderMonoidWithZeroHom.mul_comp

deleted theorem OrderMonoidWithZeroHom.toFun_eq_coe

deleted theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_coe

deleted theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_eq_coe

deleted theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_injective

deleted theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_mk

deleted def OrderMonoidWithZeroHom.toOrderMonoidHom

deleted theorem OrderMonoidWithZeroHom.toOrderMonoidHom_comp

deleted theorem OrderMonoidWithZeroHom.toOrderMonoidHom_eq_coe

deleted theorem OrderMonoidWithZeroHom.toOrderMonoidHom_injective

deleted structure OrderMonoidWithZeroHom

deleted def OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom

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

added def OrderMonoidIso.unitsWithZero

added def OrderMonoidIso.withZero

added def OrderMonoidIso.withZeroUnits

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_coe

added theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_eq_coe

added theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_injective

added theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_mk

added def OrderMonoidWithZeroHom.toOrderMonoidHom

added theorem OrderMonoidWithZeroHom.toOrderMonoidHom_comp

added theorem OrderMonoidWithZeroHom.toOrderMonoidHom_eq_coe

added theorem OrderMonoidWithZeroHom.toOrderMonoidHom_injective

added structure OrderMonoidWithZeroHom

added def OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom

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