Zulip Chat Archive
Stream: triage
Topic: PR #4707: feat(data/polynomial/reverse.lean): show traili...
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?
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?
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.
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?
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: Dec 20 2023 at 11:08 UTC