Commit 2025-08-29 12:37 c279e812

View on Github →

feat(Ideal): Add ramificationIdxIn/inertiaDegIn not zero (#29068)

Estimated changes

Modified Mathlib/NumberTheory/RamificationInertia/Basic.lean

added theorem Ideal.IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver

added theorem Ideal.inertiaDeg_ne_zero

modified theorem Ideal.inertiaDeg_pos

Modified Mathlib/NumberTheory/RamificationInertia/Galois.lean

added theorem Ideal.inertiaDegIn_ne_zero

added theorem Ideal.ramificationIdxIn_ne_zero

Modified Mathlib/RingTheory/Ideal/GoingUp.lean