Theorem NumberField.RingOfIntegers.HeightOneSpectrum.toNNReal_valued_eq_adicAbv

Modification history

2025-03-01 13:14
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
feat: `WithVal` type synonym and refactor of `HeightOneSpectrum.adicCompletion` (#22055) …
Added NumberField.RingOfIntegers.HeightOneSpectrum.toNNReal_valued_eq_adicAbvView on Github →