Zulip Chat Archive

Stream: triage

Topic: PRs #6606, #6427, #6428, #6429, #6421


Yury G. Kudryashov (Feb 10 2022 at 03:54):

I found a series of PRs #6606, #6427, #6428, #6429, #6421 by @Heather Macbeth and @Thomas Browning leading to irreducibility of xnx1x^n-x-1. What is the status? What are your plans?

Heather Macbeth (Feb 10 2022 at 03:56):

Sorry, this is my fault: I blocked Thomas' series by a new intermediate PR of my own, which spiralled into many (for which I also blame @Eric Wieser :smiley:) and which I didn't finish. I can't come back to it immediately, but perhaps in a week or so.

Thomas Browning (Feb 10 2022 at 04:44):

I'm certainly in no rush, but it would be fun to get irreducibility of xnx1x^n-x-1 into mathlib eventually. In fact, the Galois group of xnx1x^n-x-1 is SnS_n, but this might require developing a bit more algebraic number theory.

Yury G. Kudryashov (Feb 10 2022 at 05:33):

I think that we should cleanup old projects by the time we start migrating to lean 4

Yury G. Kudryashov (Feb 10 2022 at 05:34):

So today I opened several random old prs and commented or pinged someone here on zulip


Last updated: Dec 20 2023 at 11:08 UTC