Commit 2025-01-22 11:38 eb96c835

View on Github →

feat: definition of < on α ×ₗ β in partial orders (#20067) From GrowthInGroups (LeanCamCombi)

Estimated changes

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

Modified Mathlib/Algebra/Order/Rearrangement.lean

Modified Mathlib/Data/Fin/Tuple/Sort.lean

Modified Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean

Modified Mathlib/Data/Prod/Lex.lean

added theorem Prod.Lex.le_iff'

modified theorem Prod.Lex.le_iff

added theorem Prod.Lex.lt_iff'

modified theorem Prod.Lex.lt_iff

added theorem Prod.Lex.toLex_le_toLex'

added theorem Prod.Lex.toLex_le_toLex

added theorem Prod.Lex.toLex_lt_toLex'

added theorem Prod.Lex.toLex_lt_toLex

modified theorem Prod.Lex.toLex_mono

Modified Mathlib/Order/RelClasses.lean

Modified Mathlib/Order/WellFoundedSet.lean