Theorem Ideal.ramificationIdxIn_mul_ramificationIdxIn

Modification history

2026-06-18 11:44
Mathlib/NumberTheory/RamificationInertia/Galois.lean
feat(NumberTheory/RamificationInertia/Galois): ramification inertia refactor (#40126) …
Modified Ideal.ramificationIdxIn_mul_ramificationIdxInView 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.ramificationIdxIn_mul_ramificationIdxInView on Github →