Commit 2025-11-27 16:30 2b4fa094

View on Github →

feat: generalize Finsupp.lex_lt_iff_of_unique (#30973)

Estimated changes

Modified Mathlib/Data/DFinsupp/Lex.lean

added theorem DFinsupp.lex_iff_of_unique

added theorem DFinsupp.lex_le_iff_of_unique

added theorem DFinsupp.lex_lt_iff_of_unique

Modified Mathlib/Data/Finsupp/Lex.lean

added theorem Finsupp.lex_iff_of_unique

modified theorem Finsupp.lex_le_iff_of_unique

modified theorem Finsupp.lex_lt_iff_of_unique

Modified Mathlib/Order/PiLex.lean

added theorem Pi.colex_le_iff_of_unique

added theorem Pi.colex_lt_iff_of_unique

added theorem Pi.lex_iff_of_unique

added theorem Pi.lex_le_iff_of_unique

added theorem Pi.lex_lt_iff_of_unique