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

[Merged by Bors] - feat(number_theory/prime_counting): The prime counting function #9080

Closed
wants to merge 267 commits into from
Closed

[Merged by Bors] - feat(number_theory/prime_counting): The prime counting function #9080

wants to merge 267 commits into from

Conversation

BoltonBailey
Copy link
Collaborator

@BoltonBailey BoltonBailey commented Sep 8, 2021 •
edited by github-actions bot
Loading

SymmetryUnbroken and others added 30 commits August 21, 2021 13:05
@SymmetryUnbroken
Merge branch 'count' of https://github.com/leanprover-community/mathlib…
c0c0d6e 
… into count
@kim-em
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
@kim-em
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
@YaelDillies
Merge branch 'count' of https://github.com/leanprover-community/mathlib…
ff7a9f1 
… into count
@kmill
Merge branch 'count' of https://github.com/leanprover-community/mathlib…
4866256 
… into count
@kmill
fixed errors
4b7ebef
@kmill
moved count_succ_eq_succ_count_iff to where it could be proved
3bb8df2
@kmill
same thing for count_succ_eq_count_iff
b7c3c18
@kmill
implemented exists_gt_of_infinite just in case, even though it's not …
bbe03d3 
…used
@SymmetryUnbroken
Merge branch 'count' of https://github.com/leanprover-community/mathlib…
2550f9c 
… into count
@kmill
a little of nth_mem_of_le_card
9e012cd
@kmill
Merge branch 'count' of https://github.com/leanprover-community/mathlib…
f83a442 
… into count
@SymmetryUnbroken
remove a -1
0c0484d
@SymmetryUnbroken
Merge branch 'count' of https://github.com/leanprover-community/mathlib…
45d1fb3 
… into count
@SymmetryUnbroken
remove a -1 from order_iso_nat
05547af
@YaelDillies
prove the count_succ stuff
bac4ea2
@YaelDillies
some remaining +- 1
e308233
@ericrbg
improve count_succ + related
ce49224
@ericrbg
Merge remote-tracking branch 'refs/remotes/origin/count' into count
87a6ac9
@ericrbg
more tidying
01ae0c8
@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 Jan 28, 2022
@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 Jan 29, 2022
@BoltonBailey BoltonBailey added the awaiting-review The author would like community review of the PR label Jan 29, 2022
kmill
kmill reviewed Jan 29, 2022
View reviewed changes
Copy link
Collaborator

@kmill kmill left a comment

Choose a reason for hiding this comment

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

It looks good to me. I just noticed a few places that commonly might be implicit arguments.

src/data/nat/totient.lean Outdated Show resolved Hide resolved
src/data/nat/totient.lean Outdated Show resolved Hide resolved
src/number_theory/prime_counting.lean Outdated Show resolved Hide resolved
BoltonBailey and others added 5 commits January 29, 2022 12:43
@BoltonBailey @kmill
Update src/data/nat/totient.lean
9d9da9f 
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@BoltonBailey @kmill
Update src/data/nat/totient.lean
bb15b1d 
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@BoltonBailey
implicit variables
da3aa4c
@BoltonBailey
Merge branch 'BoltonBailey/prime-counting' of github.com:leanprover-c…
f4ede29 
…ommunity/mathlib into BoltonBailey/prime-counting
@BoltonBailey
fix call
b267bdf
kmill
kmill approved these changes Jan 29, 2022
View reviewed changes
Copy link
Collaborator

@kmill kmill left a comment

Choose a reason for hiding this comment

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

For the documentation, if you give fully qualified names, they'll turn into links on the website.

Once that's done, I think it's fair to say it's ready to merge (hopefully I'm doing this right 😅)

bors d=BoltonBailey

src/number_theory/prime_counting.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Jan 29, 2022

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

@leanprover-community-bot-assistant leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jan 29, 2022
@BoltonBailey @kmill
Update src/number_theory/prime_counting.lean
f678f6c 
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@bryangingechen bryangingechen changed the title feat(src/number_theory/prime_counting): The prime counting function feat(number_theory/prime_counting): The prime counting function Jan 29, 2022
@BoltonBailey
Copy link
Collaborator Author

bors r+

bors bot pushed a commit that referenced this pull request Jan 29, 2022
@BoltonBailey @SymmetryUnbroken
@kim-em @YaelDillies @kmill @ericrbg
feat(number_theory/prime_counting): The prime counting function (#9080)
4085363 
With an eye to implementing [this proof](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238002/near/251178921), I am adding a file to define the prime counting function and prove a simple upper bound on it.



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

bors bot commented Jan 29, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(number_theory/prime_counting): The prime counting function [Merged by Bors] - feat(number_theory/prime_counting): The prime counting function Jan 29, 2022
@bors bors bot closed this Jan 29, 2022
@bors bors bot deleted the BoltonBailey/prime-counting branch January 29, 2022 20:59
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@jcommelin jcommelin jcommelin left review comments

@kmill kmill kmill approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
9 participants
@BoltonBailey @leanprover-community-bot-assistant @kmill @jcommelin @SymmetryUnbroken @kim-em @YaelDillies @ericrbg @Smaug123