padicValNat_mul_pow_right — Mathlib

English

If p ≠ q are primes, then v_q(p^n q^m) = m for all n,m.

Русский

Если p и q — простые с p ≠ q, то v_q(p^n q^m) = m для всех n,m.

LaTeX

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

Lean4

theorem padicValNat_mul_pow_right {q : ℕ} [hp : Fact p.Prime] [hq : Fact q.Prime] (n m : ℕ) (neq : q ≠ p) :
    padicValNat q (p ^ n * q ^ m) = m := by
  rw [mul_comm (p ^ n) (q ^ m)]
  exact padicValNat_mul_pow_left m n neq

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