Theorem IsDedekindDomain.HeightOneSpectrum.intValuation_uniformizer

Modification history

2026-06-08 09:51
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
feat(DedekindDomain/AdicValuation): `intValuation` on uniformizers is `exp (-1)` (#37501) …
Added IsDedekindDomain.HeightOneSpectrum.intValuation_uniformizerView on Github →