Theorem NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv

Modification history

2026-03-20 17:27
Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean
chore(NumberField/FinitePlaces): generalise `RingOfIntegers K` to `R` (#36492) …
Added NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbvView on Github →