Random Issue Bot (Feb 15 2021 at 14:20):
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 (Feb 15 2021 at 14:35):
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
f to statements about the
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!
Last updated: May 09 2021 at 16:20 UTC