padicValNat_primes — Mathlib

English

If p and q are prime numbers with p ≠ q, then the p-adic valuation of q is zero.

Русский

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

LaTeX

$$$\\forall p,q \\in \\mathbb{N},\\ p\\text{ prime},\\ q\\text{ prime},\\ p \\neq q \\Rightarrow \\operatorname{padicValNat}(p,q)=0$$$

Lean4

theorem padicValNat_primes {q : ℕ} [hp : Fact p.Prime] [hq : Fact q.Prime] (neq : p ≠ q) : padicValNat p q = 0 :=
  @padicValNat.eq_zero_of_not_dvd p q <| (not_congr (Iff.symm (prime_dvd_prime_iff_eq hp.1 hq.1))).mp neq

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