Theorem Ideal.IsDedekindDomain.emultiplicity_map_eq_zero_of_ne

Modification history

2026-03-25 22:20
Mathlib/NumberTheory/RamificationInertia/Basic.lean
chore(NumberTheory/RamificationInerta/Basic): split file (#37173) …
Modified Ideal.IsDedekindDomain.emultiplicity_map_eq_zero_of_neView on Github →
2026-03-25 11:32
Mathlib/NumberTheory/RamificationInertia/Basic.lean
refactor(NumberTheory/RamificationInertia/Basic): remove the ring homomorphism from `Ideal.ramificationIdx` (#37156) …
Modified Ideal.IsDedekindDomain.emultiplicity_map_eq_zero_of_neView on Github →
2026-03-05 19:18
Mathlib/NumberTheory/RamificationInertia/Basic.lean
feat: relation between `emultiplicity` and `ramificationIdx` (#36144) …
Added Ideal.IsDedekindDomain.emultiplicity_map_eq_zero_of_neView on Github →