Commit 2026-08-17 08:31 c3d60aef
View on Github →feat(RingTheory/DedekindDomain/AdicValuation): add valuationSubring_valuation_injective (#42769)
Two injectivity lemmas on HeightOneSpectrum R. We get a unique Valuation and ValuationSubring associated to a given p : HeightOneSpectrum R.