mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard
verified publisher icon leanprover-community

feat(data/finsupp/witnesses): new file to prove results about linear orders and covariant classes in finsupps

Open adomani opened this issue 3 years ago • 1 comments

This PR proves that the lexicographic linear order on finitely supported functions preserves (one) covariant class assumption.

This is a further step in proving that many add_monoid_algebras have no zero-divisors.

  • [ ] depends on: #15984, defining the linear order on finsupps.

Open in Gitpod

adomani avatar Aug 12 '22 12:08 adomani

This PR/issue depends on:

mathlib-dependent-issues-bot avatar Aug 17 '22 04:08 mathlib-dependent-issues-bot

Besides the content of #16091, defining ne_locus, this PR introduced wit. This definition is no longer needed for its intended application, so I am closing this PR.

adomani avatar Aug 19 '22 11:08 adomani