Theorem IsLocalRing.primesOverFinset_eq

Modification history

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