of_int — Mathlib

English

The p-adic norm of an integer z satisfies padicNorm p z ≤ 1.

Русский

p-адическая норма целого числа z удовлетворяет padicNorm p z ≤ 1.

LaTeX

$$$ padicNorm\ p\ z \le 1 $$$

Lean4

/-- The `p`-adic norm of an integer is at most `1`. -/
protected theorem of_int (z : ℤ) : padicNorm p z ≤ 1 :=
  by
  obtain rfl | hz := eq_or_ne z 0
  · simp
  · rw [padicNorm, if_neg (mod_cast hz)]
    exact zpow_le_one_of_nonpos₀ (mod_cast hp.1.one_le) (by simp)

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