Theorem NumberField.vadicAbv_natCast_le_one

Modification history

2025-02-28 20:55
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
chore: renaming and documentation for `NumberField.FinitePlace` (#22407)
Deleted NumberField.vadicAbv_natCast_le_oneView on Github →
2025-02-07 08:12
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
feat(NumberTheory/NumberField/FinitePlaces): the `v`-adic absolute value induces an ultrametric distance (#21243) …
Added NumberField.vadicAbv_natCast_le_oneView on Github →