padicNorm_p_of_prime — Mathlib

English

Let p be a prime. Then the p-adic norm of p equals p^{-1} in the rational numbers.

Русский

Пусть p — простое число. Тогда p-адическая норма числа p равна p^{-1} в полях рациональных чисел.

LaTeX

$$$ padicNorm\, p\ p = (p: \mathbb{Q})^{-1} $$$

Lean4

/-- The `p`-adic norm of `p` is `p⁻¹` if `p` is prime.

See also `padicNorm.padicNorm_p` for a version assuming `1 < p`. -/
@[simp]
theorem padicNorm_p_of_prime [Fact p.Prime] : padicNorm p p = (p : ℚ)⁻¹ :=
  padicNorm_p <| Nat.Prime.one_lt Fact.out

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