padicNorm_p_lt_one_of_prime — Mathlib

English

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

Русский

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

LaTeX

$$$ Nat.Prime\ p \Rightarrow padicNorm\ p\ p < 1 $$$

Lean4

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

See also `padicNorm.padicNorm_p_lt_one` for a version assuming `1 < p`. -/
theorem padicNorm_p_lt_one_of_prime [Fact p.Prime] : padicNorm p p < 1 :=
  padicNorm_p_lt_one <| Nat.Prime.one_lt Fact.out

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