Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - chore(number_theory/legendre_symbol/quadratic_reciprocity): split some files#19193

Closed
kim-em wants to merge 2 commits intomasterfrom
split_QR
Closed

[Merged by Bors] - chore(number_theory/legendre_symbol/quadratic_reciprocity): split some files#19193
kim-em wants to merge 2 commits intomasterfrom
split_QR

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Jun 16, 2023

The best split here is separating quadratic_reciprocity into that and legendre_symbol.

I was looking at this because the olean analyser in the port-progress-bot made an unlikely claim about unnecessary dependencies, and I wanted to make sure we weren't missing something in doubting it. We weren't. :-)


Open in Gitpod

@kim-em kim-em added the awaiting-review The author would like community review of the PR label Jun 16, 2023
@jcommelin
Copy link
Copy Markdown
Member

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jun 16, 2023
bors bot pushed a commit that referenced this pull request Jun 16, 2023
…e files (#19193)

The best split here is separating `quadratic_reciprocity` into that and `legendre_symbol`.

I was looking at this because the olean analyser in the port-progress-bot made an unlikely claim about unnecessary dependencies, and I wanted to make sure we weren't missing something in doubting it. We weren't. :-)



Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
@bors
Copy link
Copy Markdown

bors bot commented Jun 16, 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 chore(number_theory/legendre_symbol/quadratic_reciprocity): split some files [Merged by Bors] - chore(number_theory/legendre_symbol/quadratic_reciprocity): split some files Jun 16, 2023
@bors bors bot closed this Jun 16, 2023
@bors bors bot deleted the split_QR branch June 16, 2023 05:28
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants