Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(Data.Nat.Multiplicity): sub_one_mul_multiplicity_factorial #6546

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(Data.Nat.Multiplicity): sub_one_mul_multiplicity_factorial #6546

wants to merge 5 commits into from

Conversation

mo271
Copy link
Collaborator

@mo271 mo271 commented Aug 12, 2023 •
edited by jcommelin

Open in Gitpod

@alreadydone alreadydone changed the title feat(Data.Nat.Multiplicity): sub_one_mul_multiplicity_factorial_eq_su… feat(Data.Nat.Multiplicity): sub_one_mul_multiplicity_factorial_eq_sub_sum_digits Aug 16, 2023
@mo271 mo271 marked this pull request as ready for review August 24, 2023 19:28
@mo271 mo271 added awaiting-review The author would like community review of the PR new-feature Add features not present in Mathlib 3 labels Aug 24, 2023
@jcommelin jcommelin added awaiting-CI and removed awaiting-review The author would like community review of the PR labels Sep 14, 2023
@mo271 mo271 added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-CI labels Sep 14, 2023
@mo271 mo271 changed the title feat(Data.Nat.Multiplicity): sub_one_mul_multiplicity_factorial_eq_sub_sum_digits feat(Data.Nat.Multiplicity): sub_one_mul_multiplicity_factorial Sep 14, 2023
@mo271 mo271 added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 14, 2023
@mo271 mo271 force-pushed the mo271/sub_one_mul_multiplicity_factorial_eq_sub_sum_digits branch from b38ccad to a925aed Compare September 15, 2023 07:01
jcommelin
jcommelin approved these changes Sep 15, 2023
View reviewed changes
Copy link
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

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Sep 15, 2023
bors bot pushed a commit that referenced this pull request Sep 15, 2023
@mo271
feat(Data.Nat.Multiplicity): sub_one_mul_multiplicity_factorial (#6546)
245441b 




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

bors bot commented Sep 15, 2023

Build failed:

@bors bors bot changed the base branch from master to ScottCarnahan/BinomialRing2 September 17, 2023 03:26
@semorrison semorrison changed the base branch from ScottCarnahan/BinomialRing2 to master September 17, 2023 12:13
@mo271
Copy link
Collaborator Author

mo271 commented Sep 17, 2023

bors r+

@bors
Copy link

bors bot commented Sep 17, 2023

🔒 Permission denied

Existing reviewers: click here to make mo271 a reviewer

@mo271
Copy link
Collaborator Author

mo271 commented Sep 17, 2023

maintainer merge

@mo271
Copy link
Collaborator Author

mo271 commented Sep 26, 2023

@jcommelin not sure what went wrong here, pinging you because I don't think there is a way for me to make bors run again...

@mo271 mo271 added the awaiting-review The author would like community review of the PR label Oct 9, 2023
@mo271
Copy link
Collaborator Author

mo271 commented Oct 9, 2023

adding the label awaiting review again so this doesn't get forgotten. Should just be ready to go...

@riccardobrasca
Copy link
Member

bors merge

@github-actions github-actions bot removed the awaiting-review The author would like community review of the PR label Oct 16, 2023
bors bot pushed a commit that referenced this pull request Oct 16, 2023
@mo271
feat(Data.Nat.Multiplicity): sub_one_mul_multiplicity_factorial (#6546)
81a8b3f 




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

bors bot commented Oct 16, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Oct 16, 2023
@mo271
feat(Data.Nat.Multiplicity): sub_one_mul_multiplicity_factorial (#6546)
7656544 




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

bors bot commented Oct 16, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Oct 16, 2023
@mo271
feat(Data.Nat.Multiplicity): sub_one_mul_multiplicity_factorial (#6546)
31656fa 




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

bors bot commented Oct 16, 2023

Build failed:

@riccardobrasca
Copy link
Member

Mmm, there is a building error here that I don't fully understand. Can you merge master and see?

bors d+

@bors
Copy link

bors bot commented Oct 16, 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.

@riccardobrasca
Copy link
Member

I read the wrong line, the error is

Error: ./././Mathlib/NumberTheory/Padics/PadicVal.lean:728:13: error: unknown identifier 'sub_one_mul_padicValNat_factorial_eq_sub_sum_digits'

so it probably just changed name or something similar.

@mo271 mo271 force-pushed the mo271/sub_one_mul_multiplicity_factorial_eq_sub_sum_digits branch from 12468bd to 1e932d9 Compare October 16, 2023 15:24
@mo271
Copy link
Collaborator Author

mo271 commented Oct 16, 2023

bors r+

bors bot pushed a commit that referenced this pull request Oct 16, 2023
@mo271
feat(Data.Nat.Multiplicity): sub_one_mul_multiplicity_factorial (#6546)
76f48d1 




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

bors bot commented Oct 16, 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(Data.Nat.Multiplicity): sub_one_mul_multiplicity_factorial [Merged by Bors] - feat(Data.Nat.Multiplicity): sub_one_mul_multiplicity_factorial Oct 16, 2023
@bors bors bot closed this Oct 16, 2023
@bors bors bot deleted the mo271/sub_one_mul_multiplicity_factorial_eq_sub_sum_digits branch October 16, 2023 22:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin Awaiting requested review from jcommelin

Assignees
No one assigned
Labels
delegated new-feature Add features not present in Mathlib 3 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.

None yet
4 participants
@mo271 @riccardobrasca @jcommelin @leanprover-community-mathlib4-bot