Skip to content

[Merged by Bors] - feat: superFactorial_dvd_vandermonde_det#6893

Closed
mo271 wants to merge 12 commits intomasterfrom
mo271/superFactorial_dvd_det_vandermonde
Closed

[Merged by Bors] - feat: superFactorial_dvd_vandermonde_det#6893
mo271 wants to merge 12 commits intomasterfrom
mo271/superFactorial_dvd_det_vandermonde

Conversation

@mo271
Copy link
Copy Markdown
Collaborator

@mo271 mo271 commented Aug 31, 2023 •
edited by github-actions bot
Loading

@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 31, 2023
@mo271 mo271 added new-feature WIP Work in progress labels Aug 31, 2023
@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 6, 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 26, 2023
@ghost
Copy link
Copy Markdown

ghost commented Sep 26, 2023

This PR/issue depends on:

@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 26, 2023
@mo271 mo271 force-pushed the mo271/superFactorial_dvd_det_vandermonde branch from a30af82 to 4b0a5fa Compare September 26, 2023 19:12
@mo271 mo271 marked this pull request as ready for review September 26, 2023 19:15
@mo271 mo271 added help-wanted The author needs attention to resolve issues awaiting-review and removed WIP Work in progress labels Sep 26, 2023
@mo271
Copy link
Copy Markdown
Collaborator Author

mo271 commented Oct 9, 2023

https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/super.20factorial.20and.20vandermonde.20determinant

@mo271 mo271 force-pushed the mo271/superFactorial_dvd_det_vandermonde branch from 958706e to 474c512 Compare November 1, 2023 20:47
github-actions[bot]
github-actions bot reviewed Nov 1, 2023
View reviewed changes
@mo271 @github-actions
Update Mathlib/Data/Nat/Factorial/SuperFactorial.lean
0f6ce43 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Vierkantor
Vierkantor reviewed Nov 2, 2023
View reviewed changes
Mathlib/Data/Nat/Factorial/SuperFactorial.lean
congr
exact Nat.descFactorial_eq_factorial_mul_choose _ _
· rw [Nat.cast_prod]

Copy link
Copy Markdown
Contributor

@Vierkantor Vierkantor Nov 2, 2023

Choose a reason for hiding this comment

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

Everything up to this point doesn't use superFactorial. Does it have any relevance outside of superfactorials? In that case, could you move it to a separate file?

Copy link
Copy Markdown
Collaborator Author

@mo271 mo271 Nov 2, 2023

Choose a reason for hiding this comment

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

I think the first four are general enough to be moved to separate LinearAlgebra/Matrix/Block and LinearAlgebra/Vandermonde resp., which I have done now. For matrixOf_eval_descPochhammer_eq_mul_matrixOf_choose seems very specific to this proof, hence I made it private.
What do you think?!
Note that for Mathlib/LinearAlgebra/Vandermonde I needed a new import.

@Vierkantor Vierkantor added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Nov 2, 2023
@mo271
Copy link
Copy Markdown
Collaborator Author

mo271 commented Nov 2, 2023 •
edited
Loading

Thanks a lot for the thorough review and nice improvements, @Vierkantor!

@mo271 mo271 added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Nov 2, 2023
Vierkantor
Vierkantor approved these changes Nov 6, 2023
View reviewed changes
Copy link
Copy Markdown
Contributor

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

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

Looks good to me, thanks!

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 6, 2023

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

@Vierkantor
Copy link
Copy Markdown
Contributor

Vierkantor commented Nov 8, 2023

Let's see if our resurrected bors works:

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Nov 8, 2023
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>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 8, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: superFactorial_dvd_vandermonde_det [Merged by Bors] - feat: superFactorial_dvd_vandermonde_det Nov 8, 2023
@mathlib-bors mathlib-bors bot closed this Nov 8, 2023
@mathlib-bors mathlib-bors bot deleted the mo271/superFactorial_dvd_det_vandermonde branch November 8, 2023 11:53
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

@github-actions github-actions[bot] github-actions[bot] left review comments

@Vierkantor Vierkantor Vierkantor approved these changes

Assignees

No one assigned

Labels

help-wanted The author needs attention to resolve issues ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@mo271 @Vierkantor