Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finsupp.to_lex_monotone

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.to_lex_monotoneView on Github →