Theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderMonoidIso_coe

Modification history

2026-10-09 07:54
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
feat: `ValuativeRel` and `IsValuativeTopology (v.adicCompletion K)` (#44279) …
Added IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderMonoidIso_coeView on Github →