Mathlib v3 is deprecated. Go to Mathlib v4

Theorem pi.lex_eq_finsupp_lex

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