Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(data/nat/choose/sum): alternating binomial coefficient sums #4997

Closed
wants to merge 4 commits into from

Conversation

awainverse
Copy link
Collaborator

Evaluates some sums related to binomial coefficients with alternating signs


Should be useful for Moebius inversion

@awainverse awainverse added the awaiting-review The author would like community review of the PR label Nov 13, 2020
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.

Mostly lgtm

src/data/nat/choose/sum.lean Show resolved Hide resolved
src/data/nat/choose/sum.lean Show resolved Hide resolved
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

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Nov 14, 2020
bors bot pushed a commit that referenced this pull request Nov 14, 2020
Evaluates some sums related to binomial coefficients with alternating signs
@awainverse
Copy link
Collaborator Author

It seems I failed to check the linter on this last theorem... can you either delegate or tell bors to merge again in a minute after I fix this?

@jcommelin
Copy link
Member

bors r-

@bors
Copy link

bors bot commented Nov 14, 2020

Canceled.

@jcommelin
Copy link
Member

bors d+

@bors
Copy link

bors bot commented Nov 14, 2020

✌️ awainverse can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@awainverse
Copy link
Collaborator Author

awainverse commented Nov 14, 2020

bors r+

bors bot pushed a commit that referenced this pull request Nov 14, 2020
Evaluates some sums related to binomial coefficients with alternating signs
@bors
Copy link

bors bot commented Nov 14, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/nat/choose/sum): alternating binomial coefficient sums [Merged by Bors] - feat(data/nat/choose/sum): alternating binomial coefficient sums Nov 14, 2020
@bors bors bot closed this Nov 14, 2020
@bors bors bot deleted the binomial_for_moebius branch November 14, 2020 22:08
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants