Johan Commelin (Mar 05 2019 at 09:02):
The splitting fields PR was just closed. What is the status of algebraic closures / galois theory / splitting fields, etc? After Lean Together I thought people decided there was a short Zorn-like argument using some sufficiently big type. But this hasn't materialized yet...
Chris Hughes (Mar 05 2019 at 09:02):
The zorn argument is much easier with direct limit I think, so I was waiting for that.
Johan Commelin (Mar 05 2019 at 09:05):
Didn't Kenny do direct limits a long time ago?
Chris Hughes (Mar 05 2019 at 09:07):
Yes, but there was something wrong with that, but I'm not sure what. There's another PR open now, but I'm putting off merging it, because I don't like having
free_comm_ring, when we already have
Kenny Lau (Mar 05 2019 at 09:12):
even when Mario said it’s alright?
Johan Commelin (Mar 05 2019 at 09:13):
I really wish these issues can be resolved soon.
Chris Hughes (Mar 05 2019 at 09:13):
I'd rather not have it there. There's no functions defined on it that don't make sense on mv polynomial.
Kevin Buzzard (Mar 05 2019 at 09:20):
So is there a PR containing both direct limits and
Chris Hughes (Mar 05 2019 at 09:21):
Kevin Buzzard (Mar 05 2019 at 09:21):
@Kenny Lau could you split it into two PR's so we can get direct limits without entering into the
Chris Hughes (Mar 05 2019 at 09:22):
Free comm ring is used for direct limit
Kevin Buzzard (Mar 05 2019 at 09:22):
Chris Hughes (Mar 05 2019 at 11:25):
@Kenny Lau Does the branch
mv_polynomial_direct_limit work? Why not use that?
Johan Commelin (Mar 07 2019 at 08:50):
I don't know anything about these issues. Is the problem once again that
mv_polynomial is to slow to be usable?
Last updated: May 11 2021 at 00:31 UTC