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)
Added 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) …
Deleted Finsupp.lex_lt_of_lt_of_preorderView on Github →
2023-02-14 10:34
Mathlib/Data/Finsupp/Lex.lean
feat: port Data.Finsupp.Lex (#2272)
Added Finsupp.lex_lt_of_lt_of_preorderView on Github →