Skip to content

[Merged by Bors] - feat: det_vandermonde_id_eq_superFactorial#6827

Closed
mo271 wants to merge 9 commits intomasterfrom
mo271/det_vandermonde_id_eq_superFactorial
Closed

[Merged by Bors] - feat: det_vandermonde_id_eq_superFactorial#6827
mo271 wants to merge 9 commits intomasterfrom
mo271/det_vandermonde_id_eq_superFactorial

Conversation

@mo271
Copy link
Copy Markdown
Collaborator

@mo271 mo271 commented Aug 28, 2023

@mo271 mo271 changed the title Mo271/det vandermonde id eq super factorial feat: det_vandermonde_id_eq_superFactorial Aug 28, 2023
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 28, 2023
@mo271 mo271 added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Aug 28, 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 Aug 28, 2023
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 10, 2023
@ghost
Copy link
Copy Markdown

ghost commented Sep 10, 2023

This PR/issue depends on:

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 10, 2023
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 10, 2023
@mo271
Copy link
Copy Markdown
Collaborator Author

mo271 commented Sep 12, 2023

will produce an easily solvable merge-conflict with #6806

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 Sep 14, 2023
bors bot pushed a commit that referenced this pull request Sep 14, 2023
- [x] depends on: #6768



Co-authored-by: Moritz Firsching <firsching@google.com>
@bors
Copy link
Copy Markdown

bors bot commented Sep 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: det_vandermonde_id_eq_superFactorial [Merged by Bors] - feat: det_vandermonde_id_eq_superFactorial Sep 14, 2023
@bors bors bot closed this Sep 14, 2023
@bors bors bot deleted the mo271/det_vandermonde_id_eq_superFactorial branch September 14, 2023 11:42
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
- [x] depends on: #6768



Co-authored-by: Moritz Firsching <firsching@google.com>
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