Theorem NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm

Modification history

2026-03-20 17:27
Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean
chore(NumberField/FinitePlaces): generalise `RingOfIntegers K` to `R` (#36492) …
Deleted NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNormView on Github →
2026-03-14 13:47
Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean
chore(NumberTheory/NumberField): move number field completion material to new subdir (#36393)
Modified NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNormView on Github →
2025-02-28 20:55
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
chore: renaming and documentation for `NumberField.FinitePlace` (#22407)
Added NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNormView on Github →