Theorem IsLocalRing.primesOver_eq

Modification history

2025-10-11 20:00
Mathlib/RingTheory/DedekindDomain/Basic.lean
feat: Ideal.ramificationIdx_mul_inertiaDeg_of_isLocalRing (#29729) …
Added IsLocalRing.primesOver_eqView on Github →