Commit 2026-04-13 19:44 4b448056

View on Github →

feat: NumberField.InfinitePlace.sum_inertiaDeg_eq_finrank (#30551) If L/K are 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.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/NumberField/Completion/InfinitePlace.lean

added theorem NumberField.InfinitePlace.Completion.liesOver_extensionEmbedding_apply

added theorem NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex_apply

added theorem NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal_apply

modified theorem NumberField.InfinitePlace.LiesOver.extensionEmbedding_liesOver_of_isReal

Created Mathlib/NumberTheory/NumberField/Completion/LiesOverInstances.lean

Created Mathlib/NumberTheory/NumberField/Completion/Ramification.lean

added theorem NumberField.InfinitePlace.Completion.finrank_eq_one_of_isUnramified

added theorem NumberField.InfinitePlace.Completion.finrank_eq_two_of_isRamified

added theorem NumberField.InfinitePlace.inertiaDeg_eq_finrank

added theorem NumberField.InfinitePlace.inertiaDeg_eq_one

added theorem NumberField.InfinitePlace.inertiaDeg_eq_two

added theorem NumberField.InfinitePlace.inertiaDeg_of_liesOver

added theorem NumberField.InfinitePlace.sum_inertiaDeg_eq_finrank