Commit 2022-09-01 11:45 44c94be8

feat(data/finsupp/lex): lexicographic orders on finsupps and covariant classes (#16127) This PR constructs a linear order on finsupps where both source and target are linearly ordered. This is useful for #15983, where these linear orders help prove that (some) add_monoid_algebras 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 This PR supersedes #15984.