Theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_eq_one_iff_not_mem

Modification history

2025-05-25 12:30
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
chore(*): not_mem/nmem -> notMem (#25159)
Deleted NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_eq_one_iff_not_memView 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_eq_one_iff_not_memView 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_eq_one_iff_not_memView on Github →