Commit 2026-07-01 14:15 25ba4967

View on Github →

chore(RingTheory/RamificationInertia/RamificationIdx): swap primes on ramificationIdx and ramificationIdx' (#41234) There's still a bit of work left to do, but I think now is a reasonable time to swap which of ramificationIdx and ramificationIdx' is primed.

Estimated changes

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

Modified Mathlib/NumberTheory/NumberField/ExistsRamified.lean

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

Modified Mathlib/NumberTheory/RamificationInertia/Basic.lean

Modified Mathlib/NumberTheory/RamificationInertia/Galois.lean

Modified Mathlib/NumberTheory/RamificationInertia/HilbertTheory.lean

Modified Mathlib/NumberTheory/RamificationInertia/Ramification.lean

added theorem Ideal.IsDedekindDomain.emultiplicity_map_eq_ramificationIdx'_mul

deleted theorem Ideal.IsDedekindDomain.emultiplicity_map_eq_ramificationIdx_mul

added theorem Ideal.IsDedekindDomain.ramificationIdx'_eq_factors_count

added theorem Ideal.IsDedekindDomain.ramificationIdx'_eq_multiplicity

added theorem Ideal.IsDedekindDomain.ramificationIdx'_eq_normalizedFactors_count

added theorem Ideal.IsDedekindDomain.ramificationIdx'_eq_one_iff

added theorem Ideal.IsDedekindDomain.ramificationIdx'_le_ramificationIdx'

added theorem Ideal.IsDedekindDomain.ramificationIdx'_ne_zero

added theorem Ideal.IsDedekindDomain.ramificationIdx'_ne_zero_of_liesOver

deleted theorem Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count

deleted theorem Ideal.IsDedekindDomain.ramificationIdx_eq_multiplicity

deleted theorem Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count

deleted theorem Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff

deleted theorem Ideal.IsDedekindDomain.ramificationIdx_le_ramificationIdx

deleted theorem Ideal.IsDedekindDomain.ramificationIdx_ne_zero

deleted theorem Ideal.IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver

added theorem Ideal.le_comap_of_ramificationIdx'_ne_zero

deleted theorem Ideal.le_comap_of_ramificationIdx_ne_zero

added theorem Ideal.le_comap_pow_ramificationIdx'

deleted theorem Ideal.le_comap_pow_ramificationIdx

added theorem Ideal.le_pow_of_le_ramificationIdx'

deleted theorem Ideal.le_pow_of_le_ramificationIdx

added theorem Ideal.le_pow_ramificationIdx'

deleted theorem Ideal.le_pow_ramificationIdx

added theorem Ideal.ramificationIdx'_algebra_tower'

added theorem Ideal.ramificationIdx'_algebra_tower

added theorem Ideal.ramificationIdx'_bot'

added theorem Ideal.ramificationIdx'_bot

added theorem Ideal.ramificationIdx'_comap_eq

added theorem Ideal.ramificationIdx'_eq_find

added theorem Ideal.ramificationIdx'_eq_one_of_map_localization

added theorem Ideal.ramificationIdx'_eq_zero

added theorem Ideal.ramificationIdx'_le_ramificationIdx'

added theorem Ideal.ramificationIdx'_lt

added theorem Ideal.ramificationIdx'_map_eq

added theorem Ideal.ramificationIdx'_map_self_eq_one

added theorem Ideal.ramificationIdx'_ne_one_iff

added theorem Ideal.ramificationIdx'_ne_zero

added theorem Ideal.ramificationIdx'_of_not_le

added theorem Ideal.ramificationIdx'_spec

deleted theorem Ideal.ramificationIdx_algebra_tower'

deleted theorem Ideal.ramificationIdx_algebra_tower

deleted theorem Ideal.ramificationIdx_bot'

deleted theorem Ideal.ramificationIdx_bot

deleted theorem Ideal.ramificationIdx_comap_eq

deleted theorem Ideal.ramificationIdx_eq_find

deleted theorem Ideal.ramificationIdx_eq_one_of_map_localization

deleted theorem Ideal.ramificationIdx_eq_zero

deleted theorem Ideal.ramificationIdx_le_ramificationIdx

deleted theorem Ideal.ramificationIdx_lt

deleted theorem Ideal.ramificationIdx_map_eq

deleted theorem Ideal.ramificationIdx_map_self_eq_one

deleted theorem Ideal.ramificationIdx_ne_one_iff

deleted theorem Ideal.ramificationIdx_ne_zero

deleted theorem Ideal.ramificationIdx_of_not_le

deleted theorem Ideal.ramificationIdx_spec

Modified Mathlib/NumberTheory/RamificationInertia/Unramified.lean

Modified Mathlib/NumberTheory/RamificationInertia/Valuation.lean

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

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

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

Modified Mathlib/RingTheory/RamificationInertia/Basic.lean

Modified Mathlib/RingTheory/RamificationInertia/Ramification.lean

deleted theorem Ideal.IsDedekindDomain.ramificationIdx'_eq_factors_count

deleted theorem Ideal.IsDedekindDomain.ramificationIdx'_eq_multiplicity

deleted theorem Ideal.IsDedekindDomain.ramificationIdx'_eq_normalizedFactors_count

added theorem Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count

added theorem Ideal.IsDedekindDomain.ramificationIdx_eq_multiplicity

added theorem Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count

deleted theorem Ideal.ramificationIdx'_above_dvd

deleted theorem Ideal.ramificationIdx'_above_le

deleted theorem Ideal.ramificationIdx'_below_dvd

deleted theorem Ideal.ramificationIdx'_below_le

deleted theorem Ideal.ramificationIdx'_def

deleted theorem Ideal.ramificationIdx'_eq

deleted theorem Ideal.ramificationIdx'_eq_one

deleted theorem Ideal.ramificationIdx'_eq_one_iff

added theorem Ideal.ramificationIdx'_eq_ramificationIdx'

added theorem Ideal.ramificationIdx'_eq_ramificationIdx

deleted theorem Ideal.ramificationIdx'_of_not_isPrime

deleted theorem Ideal.ramificationIdx'_pos

deleted theorem Ideal.ramificationIdx'_smul

deleted theorem Ideal.ramificationIdx'_tower'

deleted theorem Ideal.ramificationIdx'_tower

added theorem Ideal.ramificationIdx_above_dvd

added theorem Ideal.ramificationIdx_above_le

added theorem Ideal.ramificationIdx_below_dvd

added theorem Ideal.ramificationIdx_below_le

added theorem Ideal.ramificationIdx_def

added theorem Ideal.ramificationIdx_eq

added theorem Ideal.ramificationIdx_eq_one

added theorem Ideal.ramificationIdx_eq_one_iff

deleted theorem Ideal.ramificationIdx_eq_ramificationIdx''

deleted theorem Ideal.ramificationIdx_eq_ramificationIdx'

added theorem Ideal.ramificationIdx_of_not_isPrime

added theorem Ideal.ramificationIdx_pos

added theorem Ideal.ramificationIdx_smul

added theorem Ideal.ramificationIdx_tower'

added theorem Ideal.ramificationIdx_tower