Theorem NumberField.RingOfIntegers.HeightOneSpectrum.RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_max

Modification history

2025-02-28 20:55
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
chore: renaming and documentation for `NumberField.FinitePlace` (#22407)
Added NumberField.RingOfIntegers.HeightOneSpectrum.RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_maxView on Github →