Commit 2026-03-25 11:32 183af7ec

View on Github →

refactor(NumberTheory/RamificationInertia/Basic): remove the ring homomorphism from Ideal.ramificationIdx (#37156) This PR removes the ring homomorphism from Ideal.ramificationIdx, following the analogous refactor for Ideal.inertiaDeg in #19847. This ring homomorphism is never used in practice, and only makes statements more clunky.

Estimated changes

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

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

Modified Mathlib/NumberTheory/RamificationInertia/Basic.lean

modified theorem Ideal.IsDedekindDomain.emultiplicity_map_eq_ramificationIdx_mul

modified theorem Ideal.IsDedekindDomain.emultiplicity_map_eq_zero_of_ne

modified theorem Ideal.IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver

modified theorem Ideal.le_comap_of_ramificationIdx_ne_zero

modified theorem Ideal.le_comap_pow_ramificationIdx

modified theorem Ideal.le_pow_of_le_ramificationIdx

modified theorem Ideal.le_pow_ramificationIdx

modified theorem Ideal.ramificationIdx_bot

modified theorem Ideal.ramificationIdx_comap_eq

modified theorem Ideal.ramificationIdx_lt

modified theorem Ideal.ramificationIdx_map_eq

modified theorem Ideal.ramificationIdx_of_not_le

deleted theorem Ideal.ramificationIdx_tower

Modified Mathlib/NumberTheory/RamificationInertia/Galois.lean

Modified Mathlib/NumberTheory/RamificationInertia/Unramified.lean

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

Modified Mathlib/RingTheory/Ideal/Norm/RelNorm.lean

Modified Mathlib/RingTheory/Localization/AtPrime/Extension.lean