Theorem IsDedekindDomain.HeightOneSpectrum.eq_of_valuation_isEquiv_valuation

Modification history

2025-10-28 15:02
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
feat(RingTheory/DedekindDomain/AdicValuation): add eq_of_valuation_isEquiv_valuation (#30404)
Added IsDedekindDomain.HeightOneSpectrum.eq_of_valuation_isEquiv_valuationView on Github →