isNonarchimedean — Mathlib

English

The norm on ℂ_p is nonarchimedean.

Русский

Норма на ℂ_p является нер-архимедовой.

LaTeX

$$$\text{IsNonarchimedean}(\|\cdot\|)\;\text{on }\mathbb{C}_p.$$$

Lean4

/-- The norm on `ℂ_[p]` is nonarchimedean. -/
theorem isNonarchimedean : IsNonarchimedean (Norm.norm : ℂ_[p] → ℝ) := fun x y ↦
  by
  refine
    UniformSpace.Completion.induction_on₂ x y (isClosed_le (continuous_norm.comp continuous_add) (by fun_prop))
      (fun a b ↦ ?_)
  rw [← UniformSpace.Completion.coe_add, norm_extends, norm_extends, norm_extends]
  exact PadicAlgCl.isNonarchimedean p a b

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