padicNorm_p_lt_one — Mathlib

English

If p > 1, then the p-adic norm of p is strictly less than 1.

Русский

Если p > 1, то p-адическая норма p меньше единицы.

LaTeX

$$$ (1 < p) \rightarrow padicNorm\ p\ p < 1 $$$

Lean4

/-- The `p`-adic norm of `p` is less than `1` if `1 < p`.

See also `padicNorm.padicNorm_p_lt_one_of_prime` for a version assuming `p` is prime. -/
theorem padicNorm_p_lt_one (hp : 1 < p) : padicNorm p p < 1 :=
  by
  rw [padicNorm_p hp, inv_lt_one_iff₀]
  exact mod_cast Or.inr hp

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