Skip to content

[Merged by Bors] - feat: divRadical for polynomials#18452

Closed
seewoo5 wants to merge 15 commits intomasterfrom
feature/divradical-poly
Closed

[Merged by Bors] - feat: divRadical for polynomials#18452
seewoo5 wants to merge 15 commits intomasterfrom
feature/divradical-poly

Conversation

@seewoo5
Copy link
Copy Markdown
Collaborator

@seewoo5 seewoo5 commented Oct 30, 2024 •
edited
Loading

@seewoo5 seewoo5 added the t-algebra Algebra (groups, rings, fields, etc) label Oct 30, 2024
@seewoo5 seewoo5 requested a review from YaelDillies October 30, 2024 17:55
@seewoo5 seewoo5 self-assigned this Oct 30, 2024
@seewoo5 seewoo5 mentioned this pull request Oct 30, 2024
Closed
4 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 30, 2024 •
edited
Loading

PR summary a99e337c07

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.RingTheory.Polynomial.Radical 1130

Declarations diff

+ divRadical_dvd_derivative
+ divRadical_dvd_wronskian_left
+ divRadical_dvd_wronskian_right

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 30, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 31, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 31, 2024
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Oct 31, 2024

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 31, 2024
YaelDillies
YaelDillies reviewed Nov 1, 2024
View reviewed changes
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 1, 2024
@seewoo5 seewoo5 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 2, 2024
YaelDillies
YaelDillies reviewed Nov 2, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

maintainer merge

apart from that. Thanks!

@YaelDillies YaelDillies changed the title divRadical for polynomials feat: divRadical for polynomials Nov 2, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 2, 2024

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Nov 2, 2024
@seewoo5 @YaelDillies
Update Mathlib/RingTheory/Polynomial/Radical.lean
a99e337 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
jcommelin
jcommelin reviewed Nov 4, 2024
View reviewed changes
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 the ready-to-merge This PR has been sent to bors. label Nov 4, 2024
mathlib-bors bot pushed a commit that referenced this pull request Nov 4, 2024
@seewoo5
feat: divRadical for polynomials (#18452)
64d75cd 
Co-authored-by: Seewoo Lee <49933279+seewoo5@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 4, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: divRadical for polynomials [Merged by Bors] - feat: divRadical for polynomials Nov 4, 2024
@mathlib-bors mathlib-bors bot closed this Nov 4, 2024
@mathlib-bors mathlib-bors bot deleted the feature/divradical-poly branch November 4, 2024 09:36
@seewoo5 seewoo5 mentioned this pull request Jan 6, 2025
Closed
2 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@YaelDillies YaelDillies YaelDillies left review comments

Assignees

@seewoo5 seewoo5

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@seewoo5 @mathlib4-dependent-issues-bot @jcommelin @YaelDillies @leanprover-community-bot-assistant