Zulip Chat Archive

Stream: triage

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

view this post on Zulip 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?

view this post on Zulip 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 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!

Last updated: May 09 2021 at 16:20 UTC