Commit 2026-04-10 14:41 c98a46c4

View on Github →

feat(RamificationInertia): add ramificationIdx_le_ramificationIdx and inertiaDeg_le_inertiaDeg (#35405) Assume that Q is over P that is over p. We prove that:

Ideal.ramificationIdx P Q ≤ Ideal.ramificationIdx p Q
Ideal.inertiaDeg P Q ≤ Ideal.inertiaDeg p Q Note: These results also follow from Ideal.ramificationIdx_algebra_tower and Ideal.inertiaDeg_algebra_tower but they are proved here in a slightly more general situation.

Estimated changes

Modified Mathlib/NumberTheory/RamificationInertia/Inertia.lean

added theorem Ideal.inertiaDeg_le_inertiaDeg

Modified Mathlib/NumberTheory/RamificationInertia/Ramification.lean

added theorem Ideal.IsDedekindDomain.ramificationIdx_le_ramificationIdx

added theorem Ideal.ramificationIdx_le_ramificationIdx