Zulip Chat Archive

Stream: triage

Topic: issue #2871: unique factorisation of polynomials over a UFD

Random Issue Bot (Dec 12 2020 at 14:24):

Today I chose issue 2871 for discussion!

unique factorisation of polynomials over a UFD
Created by @Johan Commelin (@jcommelin) on 2020-05-30
Labels: feature-request

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

Johan Commelin (Dec 12 2020 at 15:36):

@Aaron Anderson is there anything left here? I don't think so, right?

Johan Commelin (Dec 12 2020 at 15:36):

So I guess we can close this issue

Aaron Anderson (Dec 12 2020 at 17:37):

You added mv_polynomials to the issue

Aaron Anderson (Dec 12 2020 at 17:38):

And I haven’t done the induction on variables, because I was hoping to do it in a super-general way instead of copy-paste

Johan Commelin (Dec 12 2020 at 17:39):

aha, makes sense

Aaron Anderson (Dec 12 2020 at 17:47):

Perhaps I should copy-paste and then make a new issue calling for the induction principle?

Johan Commelin (Dec 12 2020 at 17:50):

whatever you think is best

Johan Commelin (Dec 12 2020 at 17:50):

I think there was some chat about an induction principle recently

Johan Commelin (Dec 12 2020 at 17:50):

but I don't think it got PRd in the end

Aaron Anderson (Dec 12 2020 at 17:54):

No, it didn’t.

Aaron Anderson (Dec 12 2020 at 17:55):

I think ideally we’d have some definition of what it means to be a ring property that’s preserved under isos, but that’s got too many universe variables to be easy

Johan Commelin (Dec 12 2020 at 17:57):

well, there is the equiv_rw tactic that Scott wrote

Johan Commelin (Dec 12 2020 at 17:58):

And he has some category-theoretic machinery to support exactly this "preserved under isos" reasoning

Johan Commelin (Dec 12 2020 at 17:58):

But it hasn't seen a lot of use so far

Johan Commelin (Dec 12 2020 at 17:58):

And Scott seems to be very busy atm, so I don't think he'll be able to offer support for the time being

Random Issue Bot (Dec 28 2020 at 14:28):

Today I chose issue 2871 for discussion!

unique factorisation of polynomials over a UFD
Created by @Johan Commelin (@jcommelin) on 2020-05-30
Labels: feature-request

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

Random Issue Bot (Nov 29 2021 at 14:19):

Today I chose issue 2871 for discussion!

unique factorisation of polynomials over a UFD
Created by @Johan Commelin (@jcommelin) on 2020-05-30
Labels: feature-request

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

Johan Commelin (Nov 29 2021 at 14:24):

@Ruben Van de Velde didn't you do some stuff in this direction?

Ruben Van de Velde (Nov 29 2021 at 15:47):

Some vaguely related things - note that the issue says this is fixed for the single-variable case, but not for mv_polynomial

Random Issue Bot (Feb 11 2022 at 14:16):

Today I chose issue 2871 for discussion!

unique factorisation of polynomials over a UFD
Created by @Johan Commelin (@jcommelin) on 2020-05-30
Labels: feature-request

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

Kevin Buzzard (Feb 11 2022 at 18:27):

I added a math proof in the mv_polynomial case

Last updated: Dec 20 2023 at 11:08 UTC