Theorem Ideal.IsDedekindDomain.ramificationIdx_eq_multiplicity

Modification history

2026-03-25 22:20
Mathlib/NumberTheory/RamificationInertia/Basic.lean
chore(NumberTheory/RamificationInerta/Basic): split file (#37173) …
Modified Ideal.IsDedekindDomain.ramificationIdx_eq_multiplicityView on Github →
2025-09-16 15:34
Mathlib/NumberTheory/RamificationInertia/Basic.lean
feat(NumberField): specialized version of Kummer Dedekind for the splitting of prime numbers (#26101) …
Added Ideal.IsDedekindDomain.ramificationIdx_eq_multiplicityView on Github →