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 some lemmas about nthRootsFinset #7464

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - feat: add some lemmas about nthRootsFinset #7464

wants to merge 11 commits into from

Conversation

Ruben-VandeVelde
Copy link
Collaborator

From flt-regular.

Co-authored-by: Andrew Yang the.erd.one@gmail.com

Open in Gitpod

@Ruben-VandeVelde
feat: add some lemmas about nthRootsFinset
e2c2b15 
From flt-regular.
    
Co-authored-by: Andrew Yang <the.erd.one@gmail.com>
@Ruben-VandeVelde Ruben-VandeVelde added the awaiting-review The author would like community review of the PR label Oct 2, 2023
riccardobrasca
riccardobrasca approved these changes Oct 3, 2023
View reviewed changes
Copy link
Member

@riccardobrasca riccardobrasca left a comment •
edited

Choose a reason for hiding this comment

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

Would you mind to try to promote nthRootsFinset to a Subsemigroup? We surely need a Fintype instance, but then maybe the rest just works. (Unfortunately it is not a Submonoid in general, but it can maybe be done with neZero n).

Mathlib/Data/Polynomial/RingDivision.lean Outdated Show resolved Hide resolved
Ruben-VandeVelde and others added 2 commits October 3, 2023 21:13
@Ruben-VandeVelde
Promote
78dc272
@Ruben-VandeVelde @riccardobrasca
Update Mathlib/Data/Polynomial/RingDivision.lean
7789e39 
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Ruben-VandeVelde
Ruben-VandeVelde commented Oct 3, 2023
View reviewed changes
Mathlib/Data/Polynomial/RingDivision.lean Outdated
theorem one_mem_nthRootsFinset (hn : 0 < n) : 1 ∈ nthRootsFinset n R := by
rw [mem_nthRootsFinset hn, one_pow]

def nthRootsSubsemigroup (n : ℕ) (R : Type*) [CommRing R] [IsDomain R] : Subsemigroup R where
Copy link
Collaborator Author

Choose a reason for hiding this comment

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

@riccardobrasca was this the kind of thing you were thinking of?

Copy link
Member

Choose a reason for hiding this comment

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

I meant to change the definition of nthRootsFinset to make it a Subsemigroup instead of a Finset, so mul_mem_nthRootsFinset will be automatic. It's possible that this breaks a lot of things, in that case I don't think it is worth.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Pushed - not very excited so far. I'd like to see the impact on flt-regular before landing this.

Copy link
Member

Choose a reason for hiding this comment

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

Thanks. It should be possible to also add an instance of Submonoid provided we have NeZero n, adding an example that checks we are not creating a diamond.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

wip at https://github.com/leanprover-community/flt-regular/compare/mathlib4...nthrootfinset?expand=1

@Ruben-VandeVelde Ruben-VandeVelde 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 Oct 4, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Oct 18, 2023
@Ruben-VandeVelde Ruben-VandeVelde added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes merge-conflict The PR has a merge conflict with master, and needs manual merging. labels Nov 28, 2023
@Ruben-VandeVelde
Copy link
Collaborator Author

Would you mind to try to promote nthRootsFinset to a Subsemigroup? We surely need a Fintype instance, but then maybe the rest just works. (Unfortunately it is not a Submonoid in general, but it can maybe be done with neZero n).

I've reverted those changes because I'm not at all convinced they're making things better, especially when dealing with product over nthRootsFinset. If we want to do this, I think it should be separate from the addition of these small lemmas

@riccardobrasca
Copy link
Member

OK, no problem!

bors d+

@mathlib-bors
Copy link

mathlib-bors bot commented Nov 28, 2023

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

@github-actions github-actions bot added delegated and removed awaiting-review The author would like community review of the PR labels Nov 28, 2023
@Ruben-VandeVelde
Copy link
Collaborator Author

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Dec 3, 2023
@Ruben-VandeVelde
feat: add some lemmas about nthRootsFinset (#7464)
3e42364 
From flt-regular.
    
Co-authored-by: Andrew Yang <the.erd.one@gmail.com>
@mathlib-bors
Copy link

mathlib-bors bot commented Dec 3, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: add some lemmas about nthRootsFinset [Merged by Bors] - feat: add some lemmas about nthRootsFinset Dec 3, 2023
@mathlib-bors mathlib-bors bot closed this Dec 3, 2023
@mathlib-bors mathlib-bors bot deleted the flt-regular-nthRootsFinset branch December 3, 2023 15:25
awueth pushed a commit that referenced this pull request Dec 19, 2023
@Ruben-VandeVelde @awueth
feat: add some lemmas about nthRootsFinset (#7464)
c3df6d9 
From flt-regular.
    
Co-authored-by: Andrew Yang <the.erd.one@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@riccardobrasca riccardobrasca riccardobrasca 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
3 participants
@Ruben-VandeVelde @riccardobrasca @leanprover-community-mathlib4-bot