Commit 2026-07-14 17:49 38307016

View on Github →

feat(NumberTheory/NumberField/Completion/Ramification): add InfinitePlace.mult_mul_finrank (#41600) This PR proves that if w lies over v, then v.mult * Module.finrank v.Completion w.Completion = w.mult.

Estimated changes

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

deleted theorem NumberField.InfinitePlace.Completion.finrank_eq_one_of_isUnramified

deleted theorem NumberField.InfinitePlace.Completion.finrank_eq_two_of_isRamified

added theorem NumberField.InfinitePlace.IsRamified.finrank_eq_two

added theorem NumberField.InfinitePlace.IsUnramified.finrank_eq_one

added theorem NumberField.InfinitePlace.mult_mul_finrank

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

added theorem NumberField.InfinitePlace.IsComplex.mult_eq_two

added theorem NumberField.InfinitePlace.IsReal.mult_eq_one

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

added theorem NumberField.InfinitePlace.isUnramified_or_isRamified