Theorem Ideal.ramificationIdx_mul_inertiaDeg_of_isLocalRing

Modification history

2025-11-10 20:02
Mathlib/NumberTheory/RamificationInertia/Basic.lean
feat(RingTheory/Ideal): the inertia degree and ramification index are less than the rank (#30646) …
Modified Ideal.ramificationIdx_mul_inertiaDeg_of_isLocalRingView on Github →
2025-10-11 20:00
Mathlib/NumberTheory/RamificationInertia/Basic.lean
feat: Ideal.ramificationIdx_mul_inertiaDeg_of_isLocalRing (#29729) …
Added Ideal.ramificationIdx_mul_inertiaDeg_of_isLocalRingView on Github →