damiano
damiano
@eric-wieser, @alreadydone [This diff](https://github.com/leanprover-community/mathlib/compare/master..adomani_degree_golf) (just the file on degree of polynomials), is the kind of use that I have in mind for the lemmas in the current file. I would...
I like the point that the current definition of `max_degree` should really be named `sup_degree`. I just pushed a version containing the two options that we have been discussing. *...
@eric-wieser: #15413 Splitting seems like a very good idea!
If Ramsey's theorem has been proved in mathlib, this lemma could be an application. 🙃
@eric-wieser, here is an example of the `ne.symm` issue: ```lean import tactic.alias example {α} {a b : α} (ab : a ≠b) : b ≠a := ab.symm --works...
[docs#decidable.exists_ne](https://github.com/leanprover-community/mathlib/blob/239d882c4fb58361ee8b3b39fb2091320edef10a/src/logic/nontrivial.lean#L43), L43 is an example where dot-notation cannot be used. ```lean protected lemma decidable.exists_ne [nontrivial α] [decidable_eq α] (x : α) : ∃ y, y ≠x := begin rcases...
I've got this down to a single lemma that is still missing a one-line proof: any golfing suggestions? :smile:
> Can you copy over as many of the `pi` lemmas about lex as possible? If I understand correctly, in the `pi.lex` file there is an underlying order on the...