Skip to content

[Merged by Bors] - feat: super factorial written as product#6806

Closed
mo271 wants to merge 25 commits intomasterfrom
mo271/superFactorial_continued
Closed

[Merged by Bors] - feat: super factorial written as product#6806
mo271 wants to merge 25 commits intomasterfrom
mo271/superFactorial_continued

Conversation

@mo271
Copy link
Copy Markdown
Collaborator

@mo271 mo271 commented Aug 26, 2023 •
edited by YaelDillies
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 26, 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 26, 2023
mo271
mo271 commented Aug 28, 2023
View reviewed changes
@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
@mo271 mo271 mentioned this pull request Aug 28, 2023
Closed
@mo271 mo271 mentioned this pull request Aug 29, 2023
Closed
eric-wieser
eric-wieser reviewed Aug 30, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Aug 30, 2023
View reviewed changes
mo271 and others added 3 commits August 30, 2023 13:38
@mo271 @eric-wieser
Apply suggestions from code review
90691e9 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@mo271
fix build
a9baef3
@mo271
fix lint
f51360f
@mo271 mo271 mentioned this pull request Aug 31, 2023
Closed
5 tasks
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels 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 mo271 mentioned this pull request Sep 10, 2023
Closed
@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 19, 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 19, 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 19, 2023
@mo271 mo271 requested a review from jcommelin September 24, 2023 17:35
YaelDillies
YaelDillies reviewed Sep 25, 2023
View reviewed changes
mo271 and others added 2 commits September 25, 2023 16:53
@mo271 @YaelDillies
Update Mathlib/Data/Nat/Factorial/SuperFactorial.lean
8b3133a 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@mo271
fix proof
8bc2ba6
YaelDillies
YaelDillies reviewed Sep 25, 2023
View reviewed changes
YaelDillies
YaelDillies reviewed Sep 25, 2023
View reviewed changes
mo271 and others added 3 commits September 25, 2023 17:42
@mo271 @YaelDillies
Update Mathlib/Data/Nat/Factorial/SuperFactorial.lean
09a626f 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@mo271 @YaelDillies
Update Mathlib/Data/Nat/Factorial/SuperFactorial.lean
3ab6520 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@mo271
fix build
33482ba
YaelDillies
YaelDillies reviewed Sep 26, 2023
View reviewed changes
@mo271 @YaelDillies
Update Mathlib/Data/Nat/Factorial/SuperFactorial.lean
20ceaca 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
YaelDillies
YaelDillies reviewed Sep 26, 2023
View reviewed changes
@mo271 @YaelDillies
Update Mathlib/Data/Nat/Factorial/SuperFactorial.lean
9789542 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
YaelDillies
YaelDillies approved these changes Sep 26, 2023
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Thanks!

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Sep 26, 2023

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

@fpvandoorn
Copy link
Copy Markdown
Member

fpvandoorn commented Sep 26, 2023

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Sep 26, 2023
bors bot pushed a commit that referenced this pull request Sep 26, 2023
@mo271
feat: super factorial written as product (#6806)
0984a59 
Co-authored-by: Moritz Firsching <firsching@google.com>
@bors
Copy link
Copy Markdown

bors bot commented Sep 26, 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: super factorial written as product [Merged by Bors] - feat: super factorial written as product Sep 26, 2023
@bors bors bot closed this Sep 26, 2023
@bors bors bot deleted the mo271/superFactorial_continued branch September 26, 2023 17:40
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

@eric-wieser eric-wieser eric-wieser left review comments

@alreadydone alreadydone alreadydone left review comments

@YaelDillies YaelDillies YaelDillies approved these changes

@jcommelin jcommelin Awaiting requested review from jcommelin

Assignees

No one assigned

Labels

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.

6 participants

@mo271 @fpvandoorn @eric-wieser @alreadydone @jcommelin @YaelDillies