Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finsupp.lex_def

Modification history

2022-09-01 11:45
src/data/finsupp/lex.lean
feat(data/finsupp/lex): lexicographic orders on finsupps and covariant classes (#16127) …
Added finsupp.lex_defView on Github →