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

Stream: triage

[Yury G. Kudryashov]

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

[Heather Macbeth]

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]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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