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

[Merged by Bors] - feat(field_theory/polynomial_galois_group): New file #5861

Closed
wants to merge 21 commits into from

Conversation

tb65536
Copy link
Collaborator

@tb65536 tb65536 commented Jan 23, 2021

This PR adds the file polynomial_galois_group. It contains some of the groundwork needed for proving the Abel-Ruffini theorem.


@github-actions github-actions bot added 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. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Jan 23, 2021
@github-actions
Copy link

🎉 Great news! Looks like all the dependencies have been resolved:

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jan 27, 2021
@tb65536 tb65536 added the awaiting-review The author would like community review of the PR label Jan 27, 2021
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's a lot of really nice results packed into <250 lines!

src/field_theory/normal.lean Outdated Show resolved Hide resolved
src/field_theory/polynomial_galois_group.lean Outdated Show resolved Hide resolved
tb65536 and others added 3 commits January 27, 2021 09:38
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

lgtm

Co-authored-by: Johan Commelin <johan@commelin.net>
Copy link
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Very cool results! I just have a few organizational suggestions.

src/field_theory/polynomial_galois_group.lean Outdated Show resolved Hide resolved
src/field_theory/polynomial_galois_group.lean Outdated Show resolved Hide resolved
src/field_theory/polynomial_galois_group.lean Outdated Show resolved Hide resolved
tb65536 and others added 5 commits January 27, 2021 12:44
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Copy link
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks very good, thanks!

bors d+

@bors
Copy link

bors bot commented Jan 29, 2021

✌️ tb65536 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

tb65536 and others added 2 commits January 29, 2021 10:49
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@tb65536
Copy link
Collaborator Author

tb65536 commented Jan 29, 2021

bors r+

bors bot pushed a commit that referenced this pull request Jan 29, 2021
This PR adds the file `polynomial_galois_group`. It contains some of the groundwork needed for proving the Abel-Ruffini theorem.



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
@bors
Copy link

bors bot commented Jan 29, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(field_theory/polynomial_galois_group): New file [Merged by Bors] - feat(field_theory/polynomial_galois_group): New file Jan 29, 2021
@bors bors bot closed this Jan 29, 2021
@bors bors bot deleted the polynomial_galois_group branch January 29, 2021 21:13
b-mehta pushed a commit that referenced this pull request Jan 30, 2021
This PR adds the file `polynomial_galois_group`. It contains some of the groundwork needed for proving the Abel-Ruffini theorem.



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
b-mehta pushed a commit that referenced this pull request Apr 2, 2021
This PR adds the file `polynomial_galois_group`. It contains some of the groundwork needed for proving the Abel-Ruffini theorem.



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
@YaelDillies YaelDillies removed the awaiting-review The author would like community review of the PR label Nov 15, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants