Commit 2025-01-30 12:44 f17018b0

View on Github →

feat(Data/Finsupp/MonomialOrder) : lexicographic order on Unique (#20699) Two lemmas for lexicographic order on aUnique type are added.

Estimated changes

Modified Mathlib/Data/Finsupp/Lex.lean

added theorem Finsupp.lex_le_iff_of_unique

added theorem Finsupp.lex_lt_iff

added theorem Finsupp.lex_lt_iff_of_unique

Modified Mathlib/Data/Finsupp/MonomialOrder.lean

deleted theorem Finsupp.lex_le_iff

deleted theorem Finsupp.lex_lt_iff

added theorem MonomialOrder.lex_le_iff_of_unique

added theorem MonomialOrder.lex_lt_iff_of_unique