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/count): The count function on naturals #9457

Closed
wants to merge 172 commits into from
Closed

[Merged by Bors] - feat(data/nat/count): The count function on naturals #9457

wants to merge 172 commits into from

Conversation

SymmetryUnbroken
Copy link
Collaborator

@SymmetryUnbroken SymmetryUnbroken commented Sep 29, 2021 •
edited by YaelDillies

Defines nat.count a generic counting function on ℕ, computing how many numbers under k satisfy a given predicate".

Co-authored by:
Yaël Dillies, yael.dillies@gmail.com
Vladimir Goryachev, gor050299@gmail.com
Kyle Miller, kmill31415@gmail.com
Scott Morrison, scott@tqft.net
Eric Rodriguez, ericrboidi@gmail.com

nth and lemmas thereof have been split off into PR #10707

Open in Gitpod

semorrison and others added 30 commits August 20, 2021 23:07
@semorrison
initial API for count
31f4fdd
@YaelDillies
move sorry upstream
d89c989
@ericrbg
fix sorry, hopefully my local isn't broken
e5711ed
@ericrbg
some more knocked out+some fixes
43f5ee5
@semorrison
cleanup
f4b131c
@semorrison
whitespace
1ec2fd0
@YaelDillies
wipe away the wrong gc
8f3294c
@semorrison
Revert "wipe away the wrong gc"
db87e53 
This reverts commit 8f3294c.
@semorrison
fixing off by one errors
c1e83b2
@semorrison
one more off by one
0406bbb
@kmill
count_eq_card
2f1f927
@kmill
Merge branch 'count' of https://github.com/leanprover-community/mathlib…
9d4a0cf 
… into count
@SymmetryUnbroken
Merge branch 'count' of https://github.com/leanprover-community/mathlib…
febfcd5 
… into count
@YaelDillies
save back wipe away
73dbebb
@YaelDillies
Merge branch 'count' of https://github.com/leanprover-community/mathlib…
70f9554 
… into count
@SymmetryUnbroken
Merge branch 'count' of https://github.com/leanprover-community/mathlib…
b3064b1 
… into count
@semorrison
Merge remote-tracking branch 'origin/master' into count
8374b1d
@SymmetryUnbroken
Merge branch 'count' of https://github.com/leanprover-community/mathlib…
c0c0d6e 
… into count
@semorrison
fix import
6c27bf2
@SymmetryUnbroken
Merge branch 'count' of https://github.com/leanprover-community/mathlib…
ce20ad0 
… into count
@YaelDillies
not include the upper bound in count
c9e159a
@YaelDillies
Merge branch 'count' of https://github.com/leanprover-community/mathlib…
3c849aa 
… into count
@SymmetryUnbroken
Merge branch 'count' of https://github.com/leanprover-community/mathlib…
3122b4d 
… into count
@kmill
nth_mem_of_infinite_aux
7b84209
@semorrison
minor
31fac8c
@SymmetryUnbroken
Merge branch 'count' of https://github.com/leanprover-community/mathlib…
63f6e6b 
… into count
@kmill
Merge branch 'count' of https://github.com/leanprover-community/mathlib…
7b3e299 
… into count
@SymmetryUnbroken
Merge branch 'count' of https://github.com/leanprover-community/mathlib…
019e30a 
… into count
@kmill
fixed accidental breakage
28271e6
@YaelDillies
count_succ
cbd5356
BoltonBailey and others added 7 commits December 15, 2021 12:57
@BoltonBailey
Merge branch 'count' of github.com:leanprover-community/mathlib into …
c8285d4 
…count
@BoltonBailey @fpvandoorn
Update src/data/nat/count.lean
ce37307 
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
@BoltonBailey
notation
e27c6fd
@BoltonBailey
golf
7ee1076
@BoltonBailey @fpvandoorn
Update src/data/nat/count.lean
c743094 
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
@BoltonBailey
explicit way
18d0250
@BoltonBailey @fpvandoorn
Update src/data/nat/count.lean
2817500 
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
@BoltonBailey BoltonBailey added awaiting-CI The author would like to see what CI has to say before doing more work. and removed awaiting-author A reviewer has asked the author a question or requested changes labels Dec 15, 2021
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Dec 15, 2021
@BoltonBailey BoltonBailey added awaiting-review The author would like community review of the PR awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Dec 16, 2021
@BoltonBailey BoltonBailey added awaiting-CI The author would like to see what CI has to say before doing more work. and removed awaiting-author A reviewer has asked the author a question or requested changes labels Dec 17, 2021
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Dec 17, 2021
@fpvandoorn
Copy link
Member

Thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Dec 17, 2021
@YaelDillies YaelDillies changed the title feat(data/nat/count): introduce function count, prove theorems about it feat(data/nat/count): The count function on naturals Dec 17, 2021
bors bot pushed a commit that referenced this pull request Dec 17, 2021
@semorrison @YaelDillies
@ericrbg @kmill @SymmetryUnbroken
feat(data/nat/count): The count function on naturals (#9457)
8743573 
Defines `nat.count` a generic counting function on `ℕ`, computing how many numbers under `k` satisfy a given predicate".

Co-authored by:
Yaël Dillies, yael.dillies@gmail.com
Vladimir Goryachev, gor050299@gmail.com
Kyle Miller, kmill31415@gmail.com
Scott Morrison, scott@tqft.net
Eric Rodriguez, ericrboidi@gmail.com



Co-authored-by: YaelDillies <yael.dillies@gmail.com>
Co-authored-by: Eric <ericrboidi@gmail.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Vladimir Goryachev <gor050299@gmail.com>
@bors
Copy link

bors bot commented Dec 17, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/nat/count): The count function on naturals [Merged by Bors] - feat(data/nat/count): The count function on naturals Dec 17, 2021
@bors bors bot closed this Dec 17, 2021
@bors bors bot deleted the count branch December 17, 2021 13:09
bors bot pushed a commit that referenced this pull request Dec 24, 2021
@BoltonBailey @semorrison
@YaelDillies @ericrbg @kmill @SymmetryUnbroken
feat(data/nat/nth): add nth function (#10707)
c374a3b 
Split off from #9457, introduces `nth` and proves theorems about it.



Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: YaelDillies <yael.dillies@gmail.com>
Co-authored-by: Eric <ericrboidi@gmail.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Vladimir Goryachev <gor050299@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kmill kmill kmill left review comments

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

@jcommelin jcommelin jcommelin left review comments

@BoltonBailey BoltonBailey BoltonBailey left review comments

@YaelDillies YaelDillies YaelDillies left review comments

@hrmacbeth hrmacbeth hrmacbeth left review comments

@ericrbg ericrbg ericrbg left review comments

@fpvandoorn fpvandoorn fpvandoorn left review comments

Assignees
No one assigned
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
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
10 participants
@SymmetryUnbroken @BoltonBailey @jcommelin @fpvandoorn @kmill @eric-wieser @YaelDillies @hrmacbeth @ericrbg @semorrison