Theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_def

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.norm_defView on Github →
2026-03-06 15:35
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
chore: `FinitePlace.norm_def` -> `FinitePlace.norm_embedding` (#36184) …
Modified NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_defView on Github →
2026-03-06 13:45
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
chore(RingTheory/Valuation/RankOne): modify the definition of Valuation.RankOne using its range rather than its codomain (#26872) …
Modified NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_defView 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_defView 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_defView 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_defView on Github →