English
For prime p and odd p, and x,y ∈ ℕ with p ∣ x − y and p ∤ x, we have the same LTE relation as over ℤ, i.e., v_p(x^n − y^n) = v_p(x − y) + v_p(n).
Русский
Для простого p и нечетного p, при x,y ∈ ℕ с p | x−y и p ∤ x, справедлива та же формула LTE: v_p(x^n − y^n) = v_p(x − y) + v_p(n).
LaTeX
$$For p prime and Odd p, ∀ x,y ∈ ℕ, if p ∣ (x−y) and p ∤ x, then ∀ n, emultiplicity p (x^n − y^n) = emultiplicity p (x − y) + emultiplicity p n.$$
Lean4
theorem emultiplicity_pow_prime_pow_sub_pow_prime_pow (a : ℕ) :
emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p) (x - y) + a := by
induction a with
| zero => rw [Nat.cast_zero, add_zero, pow_zero, pow_one, pow_one]
| succ a h_ind =>
rw [Nat.cast_add, Nat.cast_one, ← add_assoc, ← h_ind, pow_succ, pow_mul, pow_mul]
apply emultiplicity_pow_prime_sub_pow_prime hp hp1
· rw [← geom_sum₂_mul]
exact dvd_mul_of_dvd_right hxy _
· exact fun h => hx (hp.dvd_of_dvd_pow h)
