Commit 2026-03-25 22:20 28a77d90

View on Github →

chore(NumberTheory/RamificationInerta/Basic): split file (#37173) This PR splits off the basic API for ramification index and inertia degree into separate files.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/RamificationInertia/Basic.lean

deleted theorem Ideal.IsDedekindDomain.emultiplicity_map_eq_ramificationIdx_mul

deleted theorem Ideal.IsDedekindDomain.emultiplicity_map_eq_zero_of_ne

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_ne_zero

deleted theorem Ideal.IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver

deleted theorem Ideal.absNorm_eq_pow_inertiaDeg'

deleted theorem Ideal.absNorm_eq_pow_inertiaDeg

deleted theorem Ideal.absNorm_eq_pow_inertiaDeg_of_liesOver

deleted theorem Ideal.inertiaDeg_algebraMap

deleted theorem Ideal.inertiaDeg_algebra_tower

deleted theorem Ideal.inertiaDeg_bot

deleted theorem Ideal.inertiaDeg_comap_eq

deleted theorem Ideal.inertiaDeg_map_eq

deleted theorem Ideal.inertiaDeg_ne_zero

deleted theorem Ideal.inertiaDeg_of_subsingleton

deleted theorem Ideal.inertiaDeg_pos

deleted theorem Ideal.le_comap_of_ramificationIdx_ne_zero

deleted theorem Ideal.le_comap_pow_ramificationIdx

deleted theorem Ideal.le_pow_of_le_ramificationIdx

deleted theorem Ideal.le_pow_ramificationIdx

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_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

Created Mathlib/NumberTheory/RamificationInertia/Inertia.lean

added theorem Ideal.absNorm_eq_pow_inertiaDeg'

added theorem Ideal.absNorm_eq_pow_inertiaDeg

added theorem Ideal.absNorm_eq_pow_inertiaDeg_of_liesOver

added theorem Ideal.inertiaDeg_algebraMap

added theorem Ideal.inertiaDeg_algebra_tower

added theorem Ideal.inertiaDeg_bot

added theorem Ideal.inertiaDeg_comap_eq

added theorem Ideal.inertiaDeg_map_eq

added theorem Ideal.inertiaDeg_ne_zero

added theorem Ideal.inertiaDeg_of_subsingleton

added theorem Ideal.inertiaDeg_pos

Created Mathlib/NumberTheory/RamificationInertia/Ramification.lean

added theorem Ideal.IsDedekindDomain.emultiplicity_map_eq_ramificationIdx_mul

added theorem Ideal.IsDedekindDomain.emultiplicity_map_eq_zero_of_ne

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_ne_zero

added theorem Ideal.IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver

added theorem Ideal.le_comap_of_ramificationIdx_ne_zero

added theorem Ideal.le_comap_pow_ramificationIdx

added theorem Ideal.le_pow_of_le_ramificationIdx

added 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_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