Theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_def'

Modification history

2026-03-06 15:35

Mathlib/NumberTheory/NumberField/FinitePlaces.lean

chore: `FinitePlace.norm_def` -> `FinitePlace.norm_embedding` (#36184) …

Deleted NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_def'View on Github →

2026-03-02 10:51

Mathlib/NumberTheory/NumberField/FinitePlaces.lean

refactor: use 1-field structure to define the `WithVal` type synonym (#34049) …

Modified NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_def'View on Github →

2025-03-01 13:14

Mathlib/NumberTheory/NumberField/FinitePlaces.lean

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

Modified NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_def'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.norm_def'View on Github →