Skip to content

[Merged by Bors] - feat: det_vandermonde_add and det_vandermonde_sub#6812

Closed
mo271 wants to merge 5 commits intomasterfrom
mo271/det_vandermonde_eq_det_vandermonde_add
Closed

[Merged by Bors] - feat: det_vandermonde_add and det_vandermonde_sub#6812
mo271 wants to merge 5 commits intomasterfrom
mo271/det_vandermonde_eq_det_vandermonde_add

Conversation

@mo271
Copy link
Copy Markdown
Collaborator

@mo271 mo271 commented Aug 27, 2023


Open in Gitpod

Co-authored-by: Alex J Best <alex.j.best@gmail.com>
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Sep 6, 2023
@alexjbest
Copy link
Copy Markdown
Member

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Sep 6, 2023

🚀 Pull request has been placed on the maintainer queue by alexjbest.

@alexjbest
Copy link
Copy Markdown
Member

Actually please delegate until the last issue is fixed

Co-authored-by: Alex J Best <alex.j.best@gmail.com>
@mo271 mo271 changed the title feat: det_vandermonde_eq_det_vandermonde_add feat: det_vandermonde_add and det_vandermonde_sub Sep 6, 2023
@kmill
Copy link
Copy Markdown
Contributor

kmill commented Sep 6, 2023

Thanks!

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Sep 6, 2023
bors bot pushed a commit that referenced this pull request Sep 6, 2023
Co-authored-by: Moritz Firsching <firsching@google.com>
@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 2023

Build failed (retrying...):

  • Build

bors bot pushed a commit that referenced this pull request Sep 6, 2023
Co-authored-by: Moritz Firsching <firsching@google.com>
@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 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_add and det_vandermonde_sub [Merged by Bors] - feat: det_vandermonde_add and det_vandermonde_sub Sep 6, 2023
@bors bors bot closed this Sep 6, 2023
@bors bors bot deleted the mo271/det_vandermonde_eq_det_vandermonde_add branch September 6, 2023 14:44
ebab pushed a commit that referenced this pull request Sep 11, 2023
Co-authored-by: Moritz Firsching <firsching@google.com>
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
Co-authored-by: Moritz Firsching <firsching@google.com>
mathlib-bors bot pushed a commit that referenced this pull request Nov 8, 2023
- [x] depends on: #6806
- [x] depends on: #6812 
- [x] depends on: #6918
- [x] depends on: #6927
- [x] depends on: #6929



Co-authored-by: Moritz Firsching <firsching@google.com>
grunweg pushed a commit that referenced this pull request Dec 15, 2023
- [x] depends on: #6806
- [x] depends on: #6812 
- [x] depends on: #6918
- [x] depends on: #6927
- [x] depends on: #6929



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.

4 participants