instIsAbsoluteValueRat — Mathlib

English

The p-adic norm defines an absolute value on ℚ: it is nonnegative, zero only at zero, satisfies the triangle inequality, and is multiplicative.

Русский

p-адическая норма образует абсолютную величину на ℚ: неотрицательна, равна нулю только в нуле, удовлетворяет неравенству треугольника и является мультипликативной.

LaTeX

$$$ \text{IsAbsoluteValue}(\, padicNorm\ p\,) $$$

Lean4

/-- The `p`-adic norm is an absolute value: positive-definite and multiplicative, satisfying the
triangle inequality. -/
instance : IsAbsoluteValue (padicNorm p) where
  abv_nonneg' := padicNorm.nonneg
  abv_eq_zero' := ⟨zero_of_padicNorm_eq_zero, fun hx ↦ by simp [hx]⟩
  abv_add' := padicNorm.triangle_ineq
  abv_mul' := padicNorm.mul

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