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