Theorem Ideal.inertiaDegIn_eq_inertiaDeg

Modification history

2026-02-18 13:41
Mathlib/NumberTheory/RamificationInertia/Galois.lean
chore(RamificationInertia): remove an unnecessary hypothesis in `inertiaDeg_algebraMap` (#35483)
Modified Ideal.inertiaDegIn_eq_inertiaDegView 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_eq_inertiaDegView on Github →
2025-02-13 06:13
Mathlib/NumberTheory/RamificationInertia/Galois.lean
feat(NumberTheory/RamificationInertia): `ramificationIdx` and `inertiaDeg` in Galois extensions (#20899) …
Added Ideal.inertiaDegIn_eq_inertiaDegView on Github →