instNontriviallyNormedField — Mathlib

English

There exists a nontrivial element with norm not equal to 1, showing the normed field is nontrivial.

Русский

Существует ненулевой элемент с ненулевой нормой, что демонстрирует немонотонность нормы.

LaTeX

$$NontriviallyNormedField(ℚ_p)$$

Lean4

instance : NontriviallyNormedField ℚ_[p] :=
  { Padic.normedField p with
    non_trivial :=
      ⟨p⁻¹, by
        rw [norm_inv, norm_p, inv_inv]
        exact mod_cast hp.1.one_lt⟩ }

Похожие утверждения