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(ring_theory/roots_of_unity): minimal polynomial of primitive roots #5322

Closed
wants to merge 8 commits into from

Conversation

riccardobrasca
Copy link
Member

I've added some simple results about the minimal polynomial of a primitive root of unity. The next step will be to prove that any two primitive roots have the same minimal polynomial.

@riccardobrasca riccardobrasca added the awaiting-review The author would like community review of the PR label Dec 11, 2020
src/ring_theory/roots_of_unity.lean Outdated Show resolved Hide resolved
src/ring_theory/roots_of_unity.lean Outdated Show resolved Hide resolved
src/ring_theory/roots_of_unity.lean Outdated Show resolved Hide resolved
src/ring_theory/roots_of_unity.lean Outdated Show resolved Hide resolved
src/ring_theory/roots_of_unity.lean Outdated Show resolved Hide resolved
src/ring_theory/roots_of_unity.lean Outdated Show resolved Hide resolved
src/ring_theory/roots_of_unity.lean Outdated Show resolved Hide resolved
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Dec 12, 2020
riccardobrasca and others added 4 commits December 12, 2020 12:20
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
@riccardobrasca riccardobrasca mentioned this pull request Dec 12, 2020
3 tasks
@riccardobrasca riccardobrasca added WIP Work in progress and removed awaiting-author A reviewer has asked the author a question or requested changes labels Dec 12, 2020
@jcommelin jcommelin changed the title feat(ring_theory.roots_of_unity): minimal polynomial of primitive roots feat(ring_theory/roots_of_unity): minimal polynomial of primitive roots Dec 12, 2020
@riccardobrasca riccardobrasca added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Dec 14, 2020
@riccardobrasca
Copy link
Member Author

I now use the general results about minimal polynomials over GCD domain, making this PR really small :)

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.

Small PRs are fine.

Thanks! 🎉

bors d+

src/ring_theory/roots_of_unity.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Dec 15, 2020

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

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

bors r+

bors bot pushed a commit that referenced this pull request Dec 15, 2020
…ts (#5322)

I've added some simple results about the minimal polynomial of a primitive root of unity. The next step will be to prove that any two primitive roots have the same minimal polynomial.
@bors
Copy link

bors bot commented Dec 15, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(ring_theory/roots_of_unity): minimal polynomial of primitive roots [Merged by Bors] - feat(ring_theory/roots_of_unity): minimal polynomial of primitive roots Dec 15, 2020
@bors bors bot closed this Dec 15, 2020
@bors bors bot deleted the min_poly_prim_root branch December 15, 2020 16:43
@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

3 participants