Zulip Chat Archive

Stream: triage

Topic: PR #4707: feat(data/polynomial/reverse.lean): show traili...


view this post on Zulip Random Issue Bot (Jan 05 2021 at 14:29):

Today I chose PR 4707 for discussion!

feat(data/polynomial/reverse.lean): show trailing_coeff is a multiplicative homomorphism
Created by @damiano (@adomani) on 2020-10-20
Labels: WIP, merge-conflict

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

view this post on Zulip Random Issue Bot (Jan 24 2021 at 14:44):

Today I chose PR 4707 for discussion!

feat(data/polynomial/reverse.lean): show trailing_coeff is a multiplicative homomorphism
Created by @damiano (@adomani) on 2020-10-20
Labels: WIP, merge-conflict

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

view this post on Zulip Damiano Testa (Jan 24 2021 at 14:53):

I have not looked at this in a while. I liked the idea of using dual_order, but had failed proving the relation between nat_degree and nat_trailing_degree. It had been suggested using reducible, but I got sidetracked by different projects. I would still like to develop multiplicativity of trailing coefficients, though.

view this post on Zulip Random Issue Bot (Feb 28 2021 at 14:19):

Today I chose PR 4707 for discussion!

feat(data/polynomial/reverse.lean): show trailing_coeff is a multiplicative homomorphism
Created by @damiano (@adomani) on 2020-10-20
Labels: WIP, merge-conflict

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

view this post on Zulip Damiano Testa (Feb 28 2021 at 14:40):

If I understand correctly, this has now been proven, yes? I think that Thomas Browning did this. I will check and then close the PR accordingly.


Last updated: May 09 2021 at 16:20 UTC