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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat: Add lemmas about Polynomial.scaleRoots. #8653

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat: Add lemmas about Polynomial.scaleRoots. #8653

wants to merge 8 commits into from

Conversation

erdOne
Copy link
Member

@erdOne erdOne commented Nov 27, 2023

Open in Gitpod

@ericrbg ericrbg changed the title Feat: Add lemmas about Polynomial.scaleRoots. feat: Add lemmas about Polynomial.scaleRoots. Nov 28, 2023
ericrbg
ericrbg reviewed Nov 28, 2023
View reviewed changes
Copy link
Collaborator

@ericrbg ericrbg left a comment

Choose a reason for hiding this comment

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

looking pretty good!

Mathlib/RingTheory/Polynomial/ScaleRoots.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/Polynomial/ScaleRoots.lean Show resolved Hide resolved
@ericrbg
Copy link
Collaborator

ericrbg commented Nov 28, 2023

I added a couple small changes, feel free to revert them if you don't like them. I felt that it was right to prime the IsUnit version of the scaleRoots_dvd lemma, because we have the iff statement with the same requirements later on anyways. I also added some dot notation because I love that stuff.

maintainer merge

@github-actions GitHub Actions
Copy link

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

Vierkantor
Vierkantor approved these changes Nov 28, 2023
View reviewed changes
Copy link
Contributor

@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.

LGTM, thanks!

bors d+

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Nov 28, 2023

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

@erdOne
Copy link
Member Author

erdOne commented Nov 28, 2023

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Nov 28, 2023
@erdOne @ericrbg
feat: Add lemmas about Polynomial.scaleRoots. (#8653)
65fce9b 
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Nov 28, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Add lemmas about Polynomial.scaleRoots. [Merged by Bors] - feat: Add lemmas about Polynomial.scaleRoots. Nov 28, 2023
@mathlib-bors mathlib-bors bot closed this Nov 28, 2023
@mathlib-bors mathlib-bors bot deleted the erd1/scaleroots_lemmas branch November 28, 2023 11:57
awueth pushed a commit that referenced this pull request Dec 19, 2023
@erdOne @ericrbg @awueth
feat: Add lemmas about Polynomial.scaleRoots. (#8653)
b4bd398 
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ericrbg ericrbg ericrbg left review comments

@Vierkantor Vierkantor Vierkantor approved these changes

Assignees
No one assigned
Labels
delegated
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@erdOne @ericrbg @Vierkantor @leanprover-community-mathlib4-bot