Theorem Ideal.inertiaDegIn_ne_zero

Modification history

2026-06-18 11:44
Mathlib/NumberTheory/RamificationInertia/Galois.lean
feat(NumberTheory/RamificationInertia/Galois): ramification inertia refactor (#40126) …
Modified Ideal.inertiaDegIn_ne_zeroView on Github →
2026-01-13 19:40
Mathlib/NumberTheory/RamificationInertia/Galois.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …
Modified Ideal.inertiaDegIn_ne_zeroView on Github →
2025-11-09 18:05
Mathlib/NumberTheory/RamificationInertia/Galois.lean
refactor(NumberTheory/RamificationInertia/Galois): switch to `IsGaloisGroup G A B` (#30934) …
Modified Ideal.inertiaDegIn_ne_zeroView on Github →
2025-08-29 12:37
Mathlib/NumberTheory/RamificationInertia/Galois.lean
feat(Ideal): Add `ramificationIdxIn`/`inertiaDegIn` not zero (#29068)
Added Ideal.inertiaDegIn_ne_zeroView on Github →