Commit 2025-12-11 10:44 6626d3a1

View on Github →

feat: colex order on finsupps (#31019)

Estimated changes

Modified Mathlib/Data/Finsupp/Lex.lean

added theorem Finsupp.Colex.le_iff_of_unique

added theorem Finsupp.Colex.lt_iff

added theorem Finsupp.Colex.lt_iff_of_unique

added theorem Finsupp.Colex.single_le_iff

added theorem Finsupp.Colex.single_lt_iff

added theorem Finsupp.Colex.single_strictMono

deleted theorem Finsupp.Lex.lt_of_lt_of_preorder

added theorem Finsupp.lex_lt_of_lt_of_preorder

added theorem Finsupp.toColex_monotone

Modified Mathlib/Order/Synonym.lean