Theorem IsDedekindDomain.HeightOneSpectrum.valuation_eq_one_iff_notMem

Modification history

2026-04-14 10:54
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
feat(RingTheory): Order of vanishing in a discrete valuation ring (#29550) …
Added IsDedekindDomain.HeightOneSpectrum.valuation_eq_one_iff_notMemView on Github →