mathlib3

44c94be8 - feat(data/finsupp/lex): lexicographic orders on finsupps and covariant classes (#16127)

feat(data/finsupp/lex): lexicographic orders on finsupps and covariant classes (#16127) This PR constructs a linear order on `finsupp`s where both source and target are linearly ordered. This is useful for #15983, where these linear orders help prove that (some) `add_monoid_algebra`s have no non-trivial zero-divisors. The PR also proves that the lexicographic linear order on finitely supported functions preserves a few covariant class assumptions. As always, comments and suggestions are really really appreciated! [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/linear.20order.20on.20finsupps) This PR supersedes #15984.