Skip to content

feat: NumberField.InfinitePlace.sum_inertiaDeg_eq_finrank#30551

Open
smmercuri wants to merge 200 commits intoleanprover-community:masterfrom
smmercuri:InfinitePlaceDim
Open

feat: NumberField.InfinitePlace.sum_inertiaDeg_eq_finrank#30551
smmercuri wants to merge 200 commits intoleanprover-community:masterfrom
smmercuri:InfinitePlaceDim

Conversation

@smmercuri
Copy link
Copy Markdown
Collaborator

@smmercuri smmercuri commented Oct 14, 2025 •
edited
Loading

If L/K are number fields number fields and v : InfinitePlace K, then the sum of inertia degrees of w : InfinitePlace L lying over v is the degree of L over K.

Open in Gitpod

Salvatore Mercuri and others added 30 commits May 13, 2025 18:27
Dimension results for infinite place completions
1b7afe1
fix import
96a82c1
Linter fixes
3971ddc
Remove open scoped Classical
ef5bfc5
Minimize imports
714bf72
predicates for extensions of complex embeddings
1e5008c
InfinitePlace.Extension API
8cd5e33
Merge branch 'smmercuri/ComplexEmbeddingExtension' into smmercuri/Inf…
5e4705b 
…initePlaceExtension
Merge branch 'master' of https://github.com/smmercuri/mathlib4 into s…
dbe4145 
…mmercuri/InfinitePlaceExtension
Merge branch 'master' of https://github.com/smmercuri/mathlib4 into s…
c08f9aa 
…mmercuri/InfinitePlaceExtensionDim
@smmercuri
Merge branch 'master' of https://github.com/smmercuri/mathlib4 into s…
f980565 
…mmercuri/InfinitePlaceExtensionDim
@smmercuri
make isExtension a type
83c9c02
@smmercuri
use inertiaDeg
b3d6a60
@smmercuri
Refactor
1f83c53
@smmercuri
Refactor
281b19b
@smmercuri
Remove sumCompl def
47b18bf
@smmercuri
Move Completion.lean
27837f9
@smmercuri
Update Mathlib.lean
21ff23f
@smmercuri
Fix naming in Field.WithAbs
da1b191
@smmercuri
Define lifts of ring homs to AbsoluteValue.Completion
c3e0c43
@smmercuri
Merge branch 'master' of https://github.com/smmercuri/mathlib4 into s…
2395098 
…mmercuri/InfinitePlaceExtension
@smmercuri
Update infinite place extension API
3e6b674
@smmercuri
golf
fa1feae
@smmercuri
Merge branch 'WithAbs-mapOfComp' into extensionEmbeddingAlgebraMap
94fab61
@smmercuri
Add algebraMap lemmas for extensionEmbeddings
563d882
@smmercuri
Fix direction of WithAbs.equiv
82efbfd
@smmercuri
Merge branch 'master' of https://github.com/smmercuri/mathlib4 into n…
6c02074 
…aming-WithAbs
@smmercuri
Merge branch 'naming-withAbs' into WithAbs-mapOfComp
bba1e46
@smmercuri
Fix direction of WithAbs.equiv
a559958
@smmercuri
Merge branch 'WithAbs-mapOfComp' into extensionEmbeddingAlgebraMap
be63c07
@smmercuri smmercuri removed the WIP Work in progress label Mar 9, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts 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 Mar 10, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Mar 10, 2026

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

@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 Mar 10, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts 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 Mar 14, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Mar 14, 2026

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

@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 Mar 15, 2026
@smmercuri smmercuri changed the title feat: dimension formulae for infinite places above feat(NumberField/Completion/Ramification): InfinitePlace.sum_inertiaDeg_eq_finrank Mar 21, 2026
@smmercuri smmercuri changed the title feat(NumberField/Completion/Ramification): InfinitePlace.sum_inertiaDeg_eq_finrank feat: NumberField.InfinitePlace.sum_inertiaDeg_eq_finrank Mar 21, 2026
@mathlib-dependent-issues mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 21, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Mar 21, 2026

This PR/issue depends on:

@grunweg grunweg added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Mar 30, 2026
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Mar 30, 2026

Coming here from PR triage: is this PR analytic or algebraic number theorey --- can you label it accordingly, please?

@smmercuri smmercuri added the t-algebra Algebra (groups, rings, fields, etc) label Mar 31, 2026
Multramate
Multramate reviewed Mar 31, 2026
View reviewed changes
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer

@Multramate Multramate Multramate left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@MichaelStollBayreuth MichaelStollBayreuth

Labels

t-algebra Algebra (groups, rings, fields, etc) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@smmercuri @mathlib4-merge-conflict-bot @grunweg @Multramate @MichaelStollBayreuth @mathlib4-dependent-issues-bot