Theorem NumberField.one_lt_norm_nnreal

Modification history

2025-02-28 20:55
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
chore: renaming and documentation for `NumberField.FinitePlace` (#22407)
Deleted NumberField.one_lt_norm_nnrealView on Github →
2025-01-29 23:20
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
feat(NumberTheory/NumberField/FinitePlaces): change one lemma (#21187) …
Added NumberField.one_lt_norm_nnrealView on Github →