real — Mathlib

English

If f is bounded and nontrivial, then there exists a prime p such that f ≈ padic(p).

Русский

Если f ограничено и ненулевое, существует простое p, такое что f эквивариантно padic(p).

LaTeX

$$∃ p, Prime(p) ∧ f ≈ (padic p)$$

Lean4

/-- The standard absolute value on `ℚ`. We name it `real` because it corresponds to the
unique real place of `ℚ`. -/
def real : AbsoluteValue ℚ ℝ where
  toFun x := |x|
  map_mul' x y := by simp
  nonneg' x := by simp
  eq_zero' x := by simp
  add_le' x y := by simpa using abs_add_le (x : ℝ) (y : ℝ)

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