Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat(data/polynomial/trinomial): X^n - X - 1 is irreducible #6421

Closed
wants to merge 34 commits into from

Conversation

tb65536
Copy link
Collaborator

@tb65536 tb65536 commented Feb 25, 2021

Proves that X^n - X - 1 is irreducible for all n ≠ 1, following the proof given by Keith Conrad here and here.

My main motivation for proving irreducibility of this polynomial is that this polynomial is a standard example of a polynomial with Galois group S_n, and proving irreducibility is a prerequisite.

(this PR is part of the irreducibility saga)


@github-actions github-actions bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Feb 25, 2021
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Feb 26, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Feb 26, 2021
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 11, 2021
@tb65536 tb65536 closed this Jul 16, 2022
bors bot pushed a commit that referenced this pull request Jul 17, 2022
This PR adds a proves irreducibility of X^n-X-1, superseding #6421.
bors bot pushed a commit that referenced this pull request Jul 17, 2022
This PR adds a proves irreducibility of X^n-X-1, superseding #6421.
joelriou pushed a commit that referenced this pull request Jul 23, 2022
This PR adds a proves irreducibility of X^n-X-1, superseding #6421.
@tb65536 tb65536 deleted the selmer1 branch September 29, 2022 16:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. merge-conflict Please `git merge origin/master` then a bot will remove this label.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

1 participant