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

The rationals are discrete in the adeles of the rationals #256

Closed
kbuzzard opened this issue Dec 1, 2024 · 2 comments · Fixed by #266
Closed

The rationals are discrete in the adeles of the rationals #256

kbuzzard opened this issue Dec 1, 2024 · 2 comments · Fixed by #266
Assignees
@jcommelin

Comments

@kbuzzard
Copy link
Collaborator

kbuzzard commented Dec 1, 2024

Assuming Rat.AdeleRing.zero_discrete, i.e. that there's some open U in A_Q whose intersection with Q is {0}, deduce that for all rationals q there's an open V in A_Q whose intersection with Q is {q}. Proof: V=U+q.

The sorry is in NumberField/AdeleRing.lean
@github-project-automation github-project-automation bot moved this to Unclaimed in FLT Project Dec 1, 2024
@jcommelin
Copy link
Contributor

claim

@kbuzzard kbuzzard moved this from Unclaimed to Claimed in FLT Project Dec 2, 2024
jcommelin added a commit to jcommelin/FLT that referenced this issue Dec 2, 2024
@jcommelin
closes ImperialCollegeLondon#256
94a88cd
@jcommelin jcommelin mentioned this issue Dec 2, 2024
Merged
@jcommelin
Copy link
Contributor

closed by #266

kbuzzard pushed a commit that referenced this issue Dec 2, 2024
@jcommelin
closes #256 (#266)
c00cd37
@github-project-automation github-project-automation bot moved this from Claimed to Completed in FLT Project Dec 2, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@jcommelin jcommelin

Labels
None yet
Projects
FLT Project
Status: Completed
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

The rationals are discrete in the adeles of the rationals jcommelin/FLT
2 participants
@jcommelin @kbuzzard