PR #4069: added statements for trailing_degree, nat_trail...

Stream: triage

[Random Issue Bot]

Today I chose PR 4069 for discussion!

added statements for trailing_degree, nat_trailing_degree, trailing_coeff,... Many proofs are missing!
Created by @damiano (@adomani) on 2020-09-08
Labels: help wanted, incomplete, needs-documentation

Is this PR still relevant? Any recent updates? Anyone making progress?

[Damiano Testa]

The lemmas in this PR are adaptations of the lemmas that existed at the time for the leading_coefficient of a polynomial, but not for the trailing_coefficient. Now, with the definition of reflect most of these lemmas can, in theory, be proved by reducing statements about the trailing_degree of f to statements about the leading_coefficient of reflect f. The missing ingredient is a proof that leading and trailing coefficients are exchanged by reflect. An earlier proof of this fact did not use dual_order and did not make into mathlib. I was not able to make the version with order_dual to work, so I am stuck and stopped thinking about this.

The lemma that I feel should be in mathlib is the statement that the trailing degree of a product is the product of the trailing degrees (with some assumptions). There have been many refactors, since I last checked: I doubt that this result is in mathlib, but if it is, then closing this PR would be fine for me!