isNonarchimedean — Mathlib

English

The norm on PadicAlgCl p is nonarchimedean: for all x,y, ||x+y|| ≤ max(||x||,||y||).

Русский

Норма на PadicAlgCl p удовлетворяет неархимедову неравенство: для всех x,y выполняется ||x+y|| ≤ max(||x||,||y||).

LaTeX

$$$$\|x+y\| \le \max\{\|x\|, \|y\|\}\quad\text{for all } x,y \in \operatorname{PadicAlgCl}(p).$$$$

Lean4

/-- The norm on `PadicAlgCl p` is nonarchimedean. -/
theorem isNonarchimedean : IsNonarchimedean (norm : PadicAlgCl p → ℝ) :=
  isNonarchimedean_spectralNorm (K := ℚ_[p]) (L := PadicAlgCl p)

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