isAbsoluteValue — Mathlib

English

The p-adic norm satisfies the absolute value axioms: nonnegativity, zero iff zero, triangle inequality, and multiplicativity.

Русский

Падиковская норма удовлетворяет аксиомам абсолютной величины: неотрицательность, равенство нулю только нулю, треугольное неравенство и умножение сохраняется.

LaTeX

$$IsAbsoluteValue on ℚ_p given by ∥·∥_p with standard properties$$

Lean4

instance isAbsoluteValue : IsAbsoluteValue fun a : ℚ_[p] ↦ ‖a‖
    where
  abv_nonneg' := norm_nonneg
  abv_eq_zero' := norm_eq_zero
  abv_add' := norm_add_le
  abv_mul' := by simp [Norm.norm, map_mul]

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