-
Notifications
You must be signed in to change notification settings - Fork 297
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.
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
[Merged by Bors] - feat(number_theory/well_approximable): well-approximable numbers and Gallagher's zero-one law #18011
Conversation
ocfnash
commented
Dec 24, 2022
•
edited
Loading
edited
- depends on: [Merged by Bors] - feat(topology/instances/add_circle): expand API for finite-order points on the circle #17986 [though only superficially]
c987078
to
5ad3969
Compare
…Gallagher's zero-one law
5ad3969
to
73f26aa
Compare
This PR/issue depends on: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Congratulations Oliver! I left a couple of suggestions, nothing crucial.
bors d+
variables {T : ℝ} [hT : fact (0 < T)] | ||
include hT | ||
|
||
local notation a `∤` b := ¬ a ∣ b |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why isn't this a global notation? Or at least a global localized notation?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Clearly it should be but I think this is best left alone till after the port since the notation ∣
(associated with the has_dvd
typeclass) is in core.
✌️ ocfnash can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
…Gallagher's zero-one law (#18011)
Pull request successfully merged into master. Build succeeded! And happy new year! 🎉 |