Theorem NumberField.RingOfIntegers.HeightOneSpectrum.RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_one

Modification history

2026-03-07 22:10
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
feat(NumberTheory/NumberField/FinitePlaces): `Module.Finite (v.adicCompletion K) (w.adicCompletion L)` (#36067) …
Deleted NumberField.RingOfIntegers.HeightOneSpectrum.RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_oneView on Github →
2025-05-27 10:28
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
feat(RingTheory/DedekindDomain/AdicValuation): Generalize `NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv` to `IsDedekindDomain.HeightOneSpectrum.adicAbv` (#25026) …
Modified NumberField.RingOfIntegers.HeightOneSpectrum.RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_oneView on Github →
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_intCast_le_oneView on Github →