Def NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace

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.FinitePlace View on Github →

2025-02-28 20:55

Mathlib/NumberTheory/NumberField/FinitePlaces.lean

chore: renaming and documentation for `NumberField.FinitePlace` (#22407)

Added NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace View on Github →