Theorem IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap

Modification history

2026-07-09 14:13

Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

refactor(NumberTheory): make `adicCompletion` a one-field structure (#41526) …

Modified IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap View on Github →

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_algebraMap View on Github →