Commit 2025-06-16 16:23 1f40b9fe

View on Github →

feat(Algebra/Order/{Monoid,GroupWithZero}/Lex): ordered inclusions and projections of prod of ordered groups (#22420)

Estimated changes

Modified Mathlib.lean

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

added theorem LinearOrderedCommGroupWithZero.fst_comp_inl

added theorem LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ

added theorem LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex

added theorem LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ

added theorem MonoidWithZeroHom.fst_mono

added theorem MonoidWithZeroHom.inl_mono

added theorem MonoidWithZeroHom.inl_strictMono

added theorem MonoidWithZeroHom.inr_mono

added theorem MonoidWithZeroHom.inr_strictMono

added theorem MonoidWithZeroHom.snd_mono

added theorem coe_symm_toLexMulEquiv

added theorem coe_toLexMulEquiv

added theorem toEquiv_symm_toLexMulEquiv

added theorem toEquiv_toLexMulEquiv

added def toLexMulEquiv

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

added theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_coe

added theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_mk

added theorem OrderMonoidWithZeroHom.toOrderMonoidHom_comp

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

added theorem MonoidHom.fst_mono

added theorem MonoidHom.inl_mono

added theorem MonoidHom.inl_strictMono

added theorem MonoidHom.inr_mono

added theorem MonoidHom.inr_strictMono

added theorem MonoidHom.snd_mono

added theorem OrderMonoidHom.commute_inl_inr

added theorem OrderMonoidHom.commute_inlₗ_inrₗ

added def OrderMonoidHom.fst

added theorem OrderMonoidHom.fst_comp_inl

added theorem OrderMonoidHom.fst_comp_inr

added def OrderMonoidHom.fstₗ

added theorem OrderMonoidHom.fstₗ_comp_inlₗ

added def OrderMonoidHom.inl

added theorem OrderMonoidHom.inl_mul_inr_eq_mk

added def OrderMonoidHom.inlₗ

added theorem OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex

added def OrderMonoidHom.inr

added def OrderMonoidHom.inrₗ

added def OrderMonoidHom.snd

added theorem OrderMonoidHom.snd_comp_inl

added theorem OrderMonoidHom.snd_comp_inr

Created Mathlib/Order/Prod/Lex/Hom.lean

added def Prod.Lex.toLexOrderHom