Skip to content

[Merged by Bors] - feat: charZero_iff_forall_prime_ne_zero#6518

Closed
ChrisHughes24 wants to merge 3 commits intomasterfrom
charZero_iff_forall_prime_ne_zero
Closed

[Merged by Bors] - feat: charZero_iff_forall_prime_ne_zero#6518
ChrisHughes24 wants to merge 3 commits intomasterfrom
charZero_iff_forall_prime_ne_zero

Conversation

@ChrisHughes24
Copy link
Copy Markdown
Member


This is slightly misplaced in the CharP file because of import issues.

Open in Gitpod

Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Aug 14, 2023
bors bot pushed a commit that referenced this pull request Aug 14, 2023
@bors
Copy link
Copy Markdown

bors bot commented Aug 14, 2023

This PR was included in a batch that was canceled, it will be automatically retried

bors bot pushed a commit that referenced this pull request Aug 14, 2023
bors bot pushed a commit that referenced this pull request Aug 14, 2023
bors bot pushed a commit that referenced this pull request Aug 14, 2023
bors bot pushed a commit that referenced this pull request Aug 14, 2023
bors bot pushed a commit that referenced this pull request Aug 14, 2023
bors bot pushed a commit that referenced this pull request Aug 14, 2023
bors bot pushed a commit that referenced this pull request Aug 14, 2023
bors bot pushed a commit that referenced this pull request Aug 14, 2023
@bors
Copy link
Copy Markdown

bors bot commented Aug 14, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Aug 14, 2023
@bors
Copy link
Copy Markdown

bors bot commented Aug 14, 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: charZero_iff_forall_prime_ne_zero [Merged by Bors] - feat: charZero_iff_forall_prime_ne_zero Aug 14, 2023
@bors bors bot closed this Aug 14, 2023
@bors bors bot deleted the charZero_iff_forall_prime_ne_zero branch August 14, 2023 20:58
kim-em pushed a commit that referenced this pull request Aug 15, 2023
kim-em pushed a commit that referenced this pull request Aug 15, 2023
kim-em pushed a commit that referenced this pull request Aug 15, 2023
kim-em pushed a commit that referenced this pull request Aug 17, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants