Skip to content

[Merged by Bors] - feat: Criteria for X ^ n - C a to be irreducible for odd n.#9397

Closed
erdOne wants to merge 8 commits intomasterfrom
erd1/irreducibleXPowSubC
Closed

[Merged by Bors] - feat: Criteria for X ^ n - C a to be irreducible for odd n.#9397
erdOne wants to merge 8 commits intomasterfrom
erd1/irreducibleXPowSubC

Conversation

@erdOne
Copy link
Copy Markdown
Member

@erdOne erdOne commented Jan 2, 2024


Open in Gitpod

@erdOne erdOne added awaiting-review t-algebra Algebra (groups, rings, fields, etc) awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jan 4, 2024
@erdOne erdOne added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jan 4, 2024
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jan 6, 2024
@erdOne erdOne added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jan 6, 2024
Copy link
Copy Markdown
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.

Thanks 🎉

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jan 6, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jan 6, 2024
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 6, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Criteria for X ^ n - C a to be irreducible for odd n. [Merged by Bors] - feat: Criteria for X ^ n - C a to be irreducible for odd n. Jan 6, 2024
@mathlib-bors mathlib-bors bot closed this Jan 6, 2024
@mathlib-bors mathlib-bors bot deleted the erd1/irreducibleXPowSubC branch January 6, 2024 21:05
YaelDillies added a commit that referenced this pull request Jan 7, 2024
Those lemmas were very recently added in #9397. Also make them iffs and golf.

Part of #9411
mathlib-bors bot pushed a commit that referenced this pull request Jan 8, 2024
Those lemmas were very recently added in #9397. Also make them iffs and golf.

Part of #9411
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants