Theorem Ideal.inertiaDegIn_mul_inertiaDegIn

Modification history

2026-06-18 11:44
Mathlib/NumberTheory/RamificationInertia/Galois.lean
feat(NumberTheory/RamificationInertia/Galois): ramification inertia refactor (#40126) …
Modified Ideal.inertiaDegIn_mul_inertiaDegInView on Github →
2025-12-03 12:39
Mathlib/NumberTheory/RamificationInertia/Galois.lean
feat(RamificationInertia): multiplicativity of indices in a tower of Galois extensions (#32309) …
Added Ideal.inertiaDegIn_mul_inertiaDegInView on Github →