Theorem Finsupp.Lex.lt_of_lt_of_preorder

Modification history

2025-12-11 10:44
Mathlib/Data/Finsupp/Lex.lean
feat: colex order on finsupps (#31019)
Deleted Finsupp.Lex.lt_of_lt_of_preorderView on Github →
2025-11-30 12:04
Mathlib/Data/Finsupp/Lex.lean
refactor: `lex_lt` → `Lex.lt` (#32243) …
Added Finsupp.Lex.lt_of_lt_of_preorderView on Github →