damiano

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.

Good point about trailing degrees! I added the definition and the result about the trailing_degree of a product.

Sorry about the confusion: I've made a mess with Git. I will try to fix it!

In case you are curious, you can take a look at [this diff](https://github.com/leanprover-community/mathlib/compare/master..adomani_degree_golf) for an immediate application of the results in this file: proving that `degree`s of *actual* polynomials "sub-multiply",...

@alreadydone I had a similar reaction as you and if you look higher up, you'll see that Eric already made his point. I agree with Eric, though: the generic stuff...

@alreadydone I'll answer better tomorrow: I'm going to bed now! I only included one result, since I wanted to focus more on the definition, than on the lemmas. I intend...

@alreadydone I agree that, most of the times, "degree" refers to an integer associated to a (mv_)polynomial and that for such applications a linearly ordered additive commutative monoid (possibly with...

@alreadydone, maybe I should make a distinction. I personally do not even know the exact definition of `semilattice_sup` and I was viewing it as a way of generalizing a `partial_order`....

> I thought I was reviewing this PR, but actually left the comments on #15376! Would you mind addressing the relevant comments in this PR? > > I don't think...

@eric-wieser, I applied the changes that you suggested in the other PR and have closed the other PR. Sorry about the confusion: I hoped that it would create less clutter...