Commit 2025-12-02 05:38 7ede2f6a

View on Github →

feat: colex order on (dependent) finsupps (#30482)

Estimated changes

Modified Mathlib/Data/DFinsupp/Lex.lean

added theorem DFinsupp.Colex.le_iff_of_unique

added theorem DFinsupp.Colex.lt_iff

added theorem DFinsupp.colex_lt_iff_of_unique

added theorem DFinsupp.toColex_monotone

Modified Mathlib/Order/Synonym.lean