Commit 2025-11-30 12:04 99709841

View on Github →

refactor: lex_lt → Lex.lt (#32243) We place theorems about the lexicographic < relation in the Lex namespace, per Yaël's suggestion.

Estimated changes

Modified Mathlib/Data/DFinsupp/Lex.lean

added theorem DFinsupp.Lex.le_iff_of_unique

added theorem DFinsupp.Lex.lt_iff

added theorem DFinsupp.Lex.lt_iff_of_unique

deleted theorem DFinsupp.lex_le_iff_of_unique

deleted theorem DFinsupp.lex_lt_iff

deleted theorem DFinsupp.lex_lt_iff_of_unique

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

added theorem Finsupp.Lex.lt_of_lt_of_preorder

deleted theorem Finsupp.lex_le_iff_of_unique

deleted theorem Finsupp.lex_lt_iff

deleted theorem Finsupp.lex_lt_iff_of_unique

deleted theorem Finsupp.lex_lt_of_lt_of_preorder

Modified Mathlib/Data/Finsupp/MonomialOrder.lean

Modified Mathlib/Order/PiLex.lean

added theorem Pi.Colex.lt_iff_of_unique

added theorem Pi.Lex.lt_iff_of_unique

deleted theorem Pi.colex_lt_iff_of_unique

deleted theorem Pi.lex_lt_iff_of_unique