Theorem IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap

Modification history

2026-03-07 22:10
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
feat(NumberTheory/NumberField/FinitePlaces): `Module.Finite (v.adicCompletion K) (w.adicCompletion L)` (#36067) …
Added IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMapView on Github →