Skip to content

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

Closed
mo271 wants to merge 12 commits intomasterfrom
port/NumberTheory.Zsqrtd.GaussianInt
Closed

[Merged by Bors] - feat: port NumberTheory.Zsqrtd.GaussianInt#5134
mo271 wants to merge 12 commits intomasterfrom
port/NumberTheory.Zsqrtd.GaussianInt

Conversation

@mo271
Copy link
Copy Markdown
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
Copy Markdown
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
Copy Markdown
Contributor

collares commented Jun 16, 2023 •
edited
Loading

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

@mo271
Copy link
Copy Markdown
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
Copy Markdown
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 awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jun 21, 2023
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 21, 2023
urkud
urkud reviewed Jun 22, 2023
View reviewed changes
urkud
urkud reviewed Jun 22, 2023
View reviewed changes
urkud
urkud reviewed Jun 22, 2023
View reviewed changes
@urkud
Copy link
Copy Markdown
Member

urkud commented Jun 22, 2023

Otherwise LGTM. Thanks!
bors d+

@bors
Copy link
Copy Markdown

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 This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review 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
Copy Markdown
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
Copy Markdown

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>
kim-em pushed a commit that referenced this pull request Jun 23, 2023
@mo271 @Ruben-VandeVelde
@Parcly-Taxel @kim-em
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>
kim-em pushed a commit that referenced this pull request Jun 23, 2023
@mo271 @Ruben-VandeVelde
@Parcly-Taxel @kim-em
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>
kim-em pushed a commit that referenced this pull request Jun 25, 2023
@mo271 @Ruben-VandeVelde
@Parcly-Taxel @kim-em
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 This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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.

5 participants

@mo271 @collares @urkud @Ruben-VandeVelde @Parcly-Taxel