Theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_embedding'

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_embedding'View on Github →
2026-03-06 15:35
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
chore: `FinitePlace.norm_def` -> `FinitePlace.norm_embedding` (#36184) …
Added NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_embedding'View on Github →