mathlib

5c88020d - feat(data/{finsupp,pi}/lex): generalize from linear_order to partial_order (#16740)

feat(data/{finsupp,pi}/lex): generalize from linear_order to partial_order (#16740) Included in #16777. Should be closed if #16777 is merged first. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>