Commit 2025-03-01 13:14 241e3ff3

View on Github →

feat: WithVal type synonym and refactor of HeightOneSpectrum.adicCompletion (#22055)

Define the WithVal type synonym equipping a ring with a valuation
Refactor HeightOneSpectrum.adicCompletion to Valuation.Completion, making use of the Valued instance on WithVal
Fix errors generated by the above changes in mathlib

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/NumberField/FinitePlaces.lean

deleted def NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.embedding

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.embedding_apply

modified theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_def'

modified theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_def

modified theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_def_int

modified theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_eq_one_iff_not_mem

modified theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_le_one

modified theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_lt_one_iff_mem

modified theorem NumberField.RingOfIntegers.HeightOneSpectrum.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm

deleted theorem NumberField.RingOfIntegers.HeightOneSpectrum.toNNReal_Valued_eq_vadicAbv

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.toNNReal_valued_eq_adicAbv

Modified Mathlib/NumberTheory/NumberField/ProductFormula.lean

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

deleted def IsDedekindDomain.HeightOneSpectrum.adicCompletion

modified theorem IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion

modified theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def

Modified Mathlib/RingTheory/LaurentSeries.lean

Created Mathlib/Topology/Algebra/Valued/WithVal.lean

added theorem WithVal.apply_equiv

added def WithVal.equiv

added def WithVal