padicValNat_prime_prime_pow — Mathlib

English

If p is a prime and q is a different prime, then the p-adic valuation of q^n is zero for every n.

Русский

Если p и q — разные простые, то v_p(q^n) = 0 для любого n.

LaTeX

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

Lean4

theorem padicValNat_prime_prime_pow {q : ℕ} [hp : Fact p.Prime] [hq : Fact q.Prime] (n : ℕ) (neq : p ≠ q) :
    padicValNat p (q ^ n) = 0 := by
  rw [padicValNat.pow _ <| Nat.Prime.ne_zero hq.elim, padicValNat_primes neq, mul_zero]

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