Commit 2026-03-06 15:35 f8f94476

View on Github →

chore: FinitePlace.norm_def -> FinitePlace.norm_embedding (#36184) Rename FinitePlace.norm_def* to FinitePlace.norm_embedding* to accommodate a new FinitePlace.norm_def which unfolds the definition.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/FinitePlaces.lean

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

modified theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_def

deleted theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_def_int

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_embedding'

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_embedding

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_embedding_int

Modified Mathlib/Topology/Algebra/Valued/NormedValued.lean

added theorem Valued.toNormedField.norm_def