Skip to content

feat : v.adicCompletionIntegers K is compact when K is a number field #30579

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
Open
smmercuri wants to merge 52 commits into
base: master
Choose a base branch
from
Open

feat : v.adicCompletionIntegers K is compact when K is a number field #30579

smmercuri wants to merge 52 commits into from

Conversation

@smmercuri
Copy link
Collaborator

@smmercuri smmercuri commented Oct 15, 2025 •
edited
Loading

@smmercuri
adicCompletion to Q_[p] uniform equiv
a0093dc
@smmercuri
IsEquiv.uniformEquiv
6e99240
@smmercuri
Proof of surjective_padicValuation
c7b43e3
@smmercuri
refactor
fae276f
@smmercuri
WithVal uniform equivalence for equivalent valuations
7c9b775
@smmercuri
Merge branch 'WithValIsEquiv' into RatAdicCompletionIntegersResidue
81ddb5d
@smmercuri
Generalise to any R equiv to Z
d22d807
@smmercuri
Golf proofs
9bd42bc
@smmercuri
le_one lemmas for HeightOneSpectrum.valuation and specialisation to Rat
51399a2
@smmercuri
left of colon
336e7c5
@smmercuri
Merge branch 'master' of https://github.com/smmercuri/mathlib4 into W…
02b5dac 
…ithValIsEquiv
@smmercuri
Restrict to homeomorphism between padicInt and adicCompletionIntegers
4fc8f3d
@smmercuri
Remove import Mathlib
d986b34
@smmercuri
Use UniformEquiv instead of Homeomorph
d20d761
@smmercuri
Add UniformEquiv.subtype
b2f32f5
@smmercuri
Uniform equivalence between p adic integers and integers of uniform s…
079224b 
…pace completion
@smmercuri
Naming
ac72cae
@smmercuri
Merge dependent
37169c5
@smmercuri
Merge branch 'HeightOneSpectrumValuation' into RatAdicCompletionInteg…
12a8751 
…ersResidue
@smmercuri
Use nonempty instead of
76afbcc
@smmercuri
Tidy
7da851e
@smmercuri
adicCompletionIntegers is compact for number fields
f7de851
@smmercuri
Complete proof
b5f2c4d
@smmercuri
Tidy
bdc9eae
@smmercuri
Simplify proof
0591faf
@smmercuri
Merge branch 'WithValIsEquiv' into RatAdicCompletionIntegersResidue
f8e14ed
@smmercuri
Move mapEquiv
c63f013
@smmercuri
Add mapEquiv
95d47c9
@smmercuri
Merge branch 'UniformSpaceMapEquiv' into RatAdicCompletionIntegersRes…
9cbb51f 
…idue
@smmercuri
Tidy
5b1f4f9
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 19, 2025
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 2, 2026
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 2, 2026
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 4, 2026
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 5, 2026
@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Jan 6, 2026
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 9, 2026
@mathlib4-merge-conflict-bot
Copy link
Collaborator

mathlib4-merge-conflict-bot commented Jan 9, 2026

This pull request has conflicts, please merge master and resolve them.

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 15, 2026
@mathlib4-dependent-issues-bot
Copy link
Collaborator

mathlib4-dependent-issues-bot commented Jan 15, 2026 •
edited
Loading

This PR/issue depends on:

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 15, 2026
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 16, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports WIP Work in progress

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@smmercuri @mathlib4-merge-conflict-bot @mathlib4-dependent-issues-bot