padicNorm_of_prime_of_ne — Mathlib

English

If p and q are primes with p ≠ q, then the p-adic norm of q is 1.

Русский

Если p и q — простые числа и p ≠ q, то p-адическая норма q равна 1.

LaTeX

$$$ padicNorm\ p\ q = 1 $$$

Lean4

/-- The `p`-adic norm of `q` is `1` if `q` is prime and not equal to `p`. -/
theorem padicNorm_of_prime_of_ne {q : ℕ} [p_prime : Fact p.Prime] [q_prime : Fact q.Prime] (neq : p ≠ q) :
    padicNorm p q = 1 := by
  have p : padicValRat p q = 0 := mod_cast padicValNat_primes neq
  rw [padicNorm, p]
  simp [q_prime.1.ne_zero]

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