Commit 2026-03-20 17:27 5eb46c3a

View on Github →

chore(NumberField/FinitePlaces): generalise RingOfIntegers K to R (#36492) This PR slightly generalises the domain in FinitePlaces.lean from RingOfIntegers K to R such that Module.Finite ℤ R and Module.Free ℤ R. This enables these results to be applied equally to O ℚ and ℤ when K = ℚ. Many results in the file previously had the namespace NumberField.RingOfIntegers.HeightOneSpectrum. These results no longer directly use the type NumberField.RingOfIntegers, so this namespace has been renamed to NumberField.HeightOneSpectrum leading to deprecations. This PR does not remove any results, however some are moved around in the file to facilitate better namespacing and section variables. These movements are as follows:

  • FinitePlace.embedding, FinitePlace.embedding_apply and instance : Valued.v.IsRankOneDiscrete now appear at the top of the file, l. 92.
  • FinitePlace, FinitePlace.mk, IsFinitePlace, FinitePlace.isFinitePlace, isFinitePlace_iff appear later in the file starting l. 264.
  • adicAbv_add_le_max, adicAbv_natCast_le_one, adicAbv_intCast_le_one appear earlier in the file, at l. 164.

Estimated changes