padicValNat_mul_pow_left — Mathlib

English

Let p and q be primes with p ≠ q. Then v_p(p^n q^m) = n for all n,m.

Русский

Пусть p и q — простые с p ≠ q. Тогда v_p(p^n q^m) = n для всех n,m.

LaTeX

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

Lean4

theorem padicValNat_mul_pow_left {q : ℕ} [hp : Fact p.Prime] [hq : Fact q.Prime] (n m : ℕ) (neq : p ≠ q) :
    padicValNat p (p ^ n * q ^ m) = n := by
  rw [padicValNat.mul (NeZero.ne' (p ^ n)).symm (NeZero.ne' (q ^ m)).symm, padicValNat.prime_pow,
    padicValNat_prime_prime_pow m neq, add_zero]

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