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: port NumberTheory.Zsqrtd.GaussianInt #5134

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat: port NumberTheory.Zsqrtd.GaussianInt #5134

wants to merge 12 commits into from

Conversation

mo271
Copy link
Collaborator

@mo271 mo271 commented Jun 16, 2023

Open in Gitpod

@mo271 mo271 added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Jun 16, 2023
@mo271
Copy link
Collaborator Author

mo271 commented Jun 16, 2023

https://leanprover-community.github.io/mathlib-port-status/file/number_theory/zsqrtd/gaussian_int
seems to indicate that this has all dependencies ported, but it seems like it needs
https://leanprover-community.github.io/mathlib-port-status/file/number_theory/legendre_symbol/quadratic_reciprocity,
which at the time of writing has
Dependencies 16 + 2 + 1008

@collares
Copy link
Collaborator

collares commented Jun 16, 2023 •
edited

That's just because leanprover-community/mathlib#19193 hasn't been processed by mathport yet, I think.

@mo271
Copy link
Collaborator Author

mo271 commented Jun 16, 2023

ok, cool, there should be only one missing dependency, namely number_theory/zsqrtd/quadratic_reciprocity.lean for GaussianInt, I suppose

@mo271 mo271 removed the WIP Work in progress label Jun 20, 2023
@mo271
Copy link
Collaborator Author

mo271 commented Jun 20, 2023

still waiting for number_theory/legendre_symbol/quadratic_reciprocity.

Ruben-VandeVelde and others added 5 commits June 21, 2023 22:18
@Ruben-VandeVelde
feat: port NumberTheory.Zsqrtd.GaussianInt
2a9ee73
@Ruben-VandeVelde
Initial file copy from mathport
c29ffe6
@Ruben-VandeVelde
automated fixes
03de9c6 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@mo271 @Ruben-VandeVelde
starting
a74fb0f
@mo271 @Ruben-VandeVelde
first pass
9866922
@Ruben-VandeVelde Ruben-VandeVelde force-pushed the port/NumberTheory.Zsqrtd.GaussianInt branch from 4a9c5cc to 9866922 Compare June 21, 2023 20:22
@Ruben-VandeVelde Ruben-VandeVelde added awaiting-review The author would like community review of the PR awaiting-CI labels Jun 21, 2023
@urkud
Copy link
Member

urkud commented Jun 22, 2023

Otherwise LGTM. Thanks!
bors d+

@bors
Copy link

bors bot commented Jun 22, 2023

✌️ mo271 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 Jun 22, 2023
mo271 and others added 2 commits June 22, 2023 08:24
@mo271 @urkud
Apply suggestions from code review
913c450 
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@Parcly-Taxel
Update GaussianInt.lean
ddfd926
@mo271
Copy link
Collaborator Author

mo271 commented Jun 22, 2023

bors r+

bors bot pushed a commit that referenced this pull request Jun 22, 2023
@mo271 @Ruben-VandeVelde @Parcly-Taxel
feat: port NumberTheory.Zsqrtd.GaussianInt (#5134)
8a76b3e 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
@bors
Copy link

bors bot commented Jun 22, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: port NumberTheory.Zsqrtd.GaussianInt [Merged by Bors] - feat: port NumberTheory.Zsqrtd.GaussianInt Jun 22, 2023
@bors bors bot closed this Jun 22, 2023
@bors bors bot deleted the port/NumberTheory.Zsqrtd.GaussianInt branch June 22, 2023 07:57
alexkeizer pushed a commit that referenced this pull request Jun 22, 2023
@mo271 @Ruben-VandeVelde
@Parcly-Taxel @alexkeizer
feat: port NumberTheory.Zsqrtd.GaussianInt (#5134)
a1be8be 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
semorrison pushed a commit that referenced this pull request Jun 23, 2023
@mo271 @Ruben-VandeVelde
@Parcly-Taxel @semorrison
feat: port NumberTheory.Zsqrtd.GaussianInt (#5134)
f2b98ce 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
semorrison pushed a commit that referenced this pull request Jun 23, 2023
@mo271 @Ruben-VandeVelde
@Parcly-Taxel @semorrison
feat: port NumberTheory.Zsqrtd.GaussianInt (#5134)
d315225 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
semorrison pushed a commit that referenced this pull request Jun 25, 2023
@mo271 @Ruben-VandeVelde
@Parcly-Taxel @semorrison
feat: port NumberTheory.Zsqrtd.GaussianInt (#5134)
299273c 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
kbuzzard pushed a commit that referenced this pull request Jul 6, 2023
@mo271 @Ruben-VandeVelde
@Parcly-Taxel @kbuzzard
feat: port NumberTheory.Zsqrtd.GaussianInt (#5134)
62a55ad 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

Assignees
No one assigned
Labels
delegated mathlib-port This is a port of a theory file from mathlib.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@mo271 @collares @urkud @Ruben-VandeVelde @Parcly-Taxel