# Zulip Chat Archive

## Stream: general

### Topic: my_polynomial performance

#### Reid Barton (Nov 17 2018 at 19:03):

I tried proving that the polynomial ring functor is left adjoint to the forgetful functor CommRing -> Set but I gave up because doing anything with `mv_polynomial`

was so slow. @Kenny Lau you were having similar problems with `mv_polynomial`

right?

I think something is wrong there, but I couldn't figure out what.

#### Kenny Lau (Nov 17 2018 at 19:07):

yes, something is wrong

#### Kenny Lau (Nov 17 2018 at 19:07):

@Mario Carneiro what do you think?

#### Mario Carneiro (Nov 17 2018 at 23:37):

I think something is wrong

#### Kenny Lau (Nov 17 2018 at 23:40):

...

#### Mario Carneiro (Nov 17 2018 at 23:41):

my impression is that lean is having to solve enormous typeclass problems, I'm not sure if that's the whole problem

#### Kenny Lau (Nov 17 2018 at 23:42):

would you know specifically what is the problem with mv_polynomial and polynomial?

#### Mario Carneiro (Nov 17 2018 at 23:43):

if you look at the pp.all versions of any of the theorem statements, what looks like five tokens fills several pages

#### Kenny Lau (Nov 17 2018 at 23:44):

I don't think `pp.all`

tells us *all* about the situation

#### Kenny Lau (Nov 17 2018 at 23:45):

but sure it tells us a lot

#### Mario Carneiro (Nov 17 2018 at 23:45):

yeah it doesn't know when to shut up

Last updated: May 08 2021 at 04:14 UTC