Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-04 18:24 5c88020d

View on Github →

feat(data/{finsupp,pi}/lex): generalize from linear_order to partial_order (#16740) Included in #16777. Should be closed if #16777 is merged first.

Estimated changes

Modified src/data/finsupp/lex.lean

Modified src/data/pi/lex.lean

modified theorem pi.lex.le_of_forall_le

modified theorem pi.lex.le_of_of_lex_le

modified theorem pi.to_lex_monotone