Commit 2026-06-18 11:44 63b065c2

View on Github →

feat(NumberTheory/RamificationInertia/Galois): ramification inertia refactor (#40126) This is a first pass at refactoring NumberTheory/RamificationInertia/Galois to use the new definitions ramificationIdx' and inertiaDeg'. I tried to keep changes to downstream files minimal to keep this PR on the smaller side. More will be done in future PRs.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/ClassNumber.lean

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

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

modified theorem IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one'

modified theorem IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one

Modified Mathlib/NumberTheory/NumberField/ExistsRamified.lean

Modified Mathlib/NumberTheory/RamificationInertia/Galois.lean

modified theorem Ideal.card_inertia_eq_ramificationIdxIn

modified theorem Ideal.card_stabilizer_eq

modified theorem Ideal.card_stabilizer_eq_card_inertia_mul_finrank

modified theorem Ideal.inertiaDegIn_mul_inertiaDegIn

modified theorem Ideal.inertiaDegIn_ne_zero

modified theorem Ideal.ncard_primesOver_mul_card_inertia_mul_finrank

modified theorem Ideal.ncard_primesOver_mul_ncard_primesOver

deleted theorem Ideal.ramificationIdxIn_mul_ramificationIdxIn'

modified theorem Ideal.ramificationIdxIn_mul_ramificationIdxIn

modified theorem Ideal.ramificationIdxIn_ne_zero

Modified Mathlib/NumberTheory/RamificationInertia/HilbertTheory.lean

Modified Mathlib/RingTheory/Ideal/GoingUp.lean

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