Theorem NumberField.FinitePlace.norm_eq_one_iff_notMem

Modification history

2026-03-20 17:27
Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean
chore(NumberField/FinitePlaces): generalise `RingOfIntegers K` to `R` (#36492) …
Modified NumberField.FinitePlace.norm_eq_one_iff_notMemView on Github →
2026-03-14 13:47
Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean
chore(NumberTheory/NumberField): move number field completion material to new subdir (#36393)
Modified NumberField.FinitePlace.norm_eq_one_iff_notMemView on Github →
2026-03-07 22:10
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
feat(NumberTheory/NumberField/FinitePlaces): `Module.Finite (v.adicCompletion K) (w.adicCompletion L)` (#36067) …
Added NumberField.FinitePlace.norm_eq_one_iff_notMemView on Github →