Commit 2025-09-16 15:34 d36f2670

View on Github →

feat(NumberField): specialized version of Kummer Dedekind for the splitting of prime numbers (#26101) We prove a specialized version of KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk for the splitting of rational prime numbers in number fields. This PR continues the work from #25038.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/Ideal/KummerDedekind.lean

added theorem NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply'

added theorem NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply

added theorem NumberField.Ideal.liesOver_primesOverSpanEquivMonicFactorsMod_symm

added def NumberField.Ideal.primesOverSpanEquivMonicFactorsMod

added theorem NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply

added theorem NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span

added theorem NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply'

added theorem NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply

Modified Mathlib/NumberTheory/RamificationInertia/Basic.lean

added theorem Ideal.IsDedekindDomain.ramificationIdx_eq_multiplicity

Modified Mathlib/RingTheory/AdjoinRoot.lean

added theorem finrank_quotient_span_eq_natDegree

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

added theorem Ideal.mem_primesOver_iff_mem_normalizedFactors

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

added theorem finrank_quotient_span_eq_natDegree'