## 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

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

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?

Last updated: May 09 2021 at 16:20 UTC