Skip to content

[Merged by Bors] - feat: descPochhammer#6918

Closed
mo271 wants to merge 8 commits intomasterfrom
mo271/descPochhammer
Closed

[Merged by Bors] - feat: descPochhammer#6918
mo271 wants to merge 8 commits intomasterfrom
mo271/descPochhammer

Conversation

@mo271
Copy link
Copy Markdown
Collaborator

@mo271 mo271 commented Sep 1, 2023 •
edited by github-actions bot
Loading

@mo271 mo271 mentioned this pull request Sep 1, 2023
Closed
5 tasks
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 1, 2023
@mo271 mo271 added new-feature awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Sep 1, 2023
@mo271 mo271 added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Sep 1, 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 Sep 1, 2023
This was referenced Sep 2, 2023
Closed
Closed
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 12, 2023
@ghost
Copy link
Copy Markdown

ghost commented Sep 12, 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 12, 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 12, 2023
jcommelin
jcommelin approved these changes Sep 14, 2023
View reviewed changes
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.

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Sep 14, 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.

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Sep 14, 2023
@mo271 @jcommelin
Update Mathlib/RingTheory/Polynomial/Pochhammer.lean
59a8666 
Co-authored-by: Johan Commelin <johan@commelin.net>
@mo271
Copy link
Copy Markdown
Collaborator Author

mo271 commented Sep 14, 2023

bors r+

bors bot pushed a commit that referenced this pull request Sep 14, 2023
@mo271
feat: descPochhammer (#6918)
42093ba 
- [x] depends on: #6917 



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: descPochhammer [Merged by Bors] - feat: descPochhammer Sep 14, 2023
@bors bors bot closed this Sep 14, 2023
@bors bors bot deleted the mo271/descPochhammer branch September 14, 2023 12:41
bors bot pushed a commit that referenced this pull request Sep 14, 2023
@mo271
feat: monic_descPochhammer (#6927)
99256a0 
 - [x] depends on: #6918



Co-authored-by: Moritz Firsching <firsching@google.com>
bors bot pushed a commit that referenced this pull request Sep 14, 2023
@mo271
feat: descPochhammer_natDegree (#6929)
fd96e55 
- [x] depends on: #6918 



Co-authored-by: Moritz Firsching <firsching@google.com>
bors bot pushed a commit that referenced this pull request Sep 14, 2023
@mo271
feat: monic_descPochhammer (#6927)
a90843f 
 - [x] depends on: #6918



Co-authored-by: Moritz Firsching <firsching@google.com>
bors bot pushed a commit that referenced this pull request Sep 14, 2023
@mo271
feat: descPochhammer_natDegree (#6929)
c493a2c 
- [x] depends on: #6918 



Co-authored-by: Moritz Firsching <firsching@google.com>
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
@mo271 @kodyvajjha
feat: descPochhammer (#6918)
14fcc87 
- [x] depends on: #6917 



Co-authored-by: Moritz Firsching <firsching@google.com>
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
@mo271 @kodyvajjha
feat: monic_descPochhammer (#6927)
5cdfd4a 
 - [x] depends on: #6918



Co-authored-by: Moritz Firsching <firsching@google.com>
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
@mo271 @kodyvajjha
feat: descPochhammer_natDegree (#6929)
a56527c 
- [x] depends on: #6918 



Co-authored-by: Moritz Firsching <firsching@google.com>
mathlib-bors bot pushed a commit that referenced this pull request Nov 8, 2023
@mo271
feat: superFactorial_dvd_vandermonde_det (#6893)
9efe273 
- [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
@mo271 @grunweg
feat: superFactorial_dvd_vandermonde_det (#6893)
49598be 
- [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

Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer).

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@mo271 @jcommelin