English
For p a prime and odd, if p divides x − y and p does not divide x, then for any n, v_p(x^n − y^n) = v_p(x − y) + v_p(n). A parallel statement holds for sums x^n + y^n when n is odd.
Русский
Для простого p и нечетного p, если p делит x−y и p не делит x, то для любого n выполняется v_p(x^n−y^n) = v_p(x−y) + v_p(n). Аналогично для сумм при нечетном n.
LaTeX
$$For prime p and Odd p, with p ∣ (x−y) and p ∤ x, ∀ n, emultiplicity p (x^n − y^n) = emultiplicity p (x − y) + emultiplicity p n; similarly for x^n + y^n when n is odd.$$
Lean4
theorem emultiplicity_pow_sub_pow_of_prime {p : R} (hp : Prime p) {x y : R} (hxy : p ∣ x - y) (hx : ¬p ∣ x) {n : ℕ}
(hn : ¬p ∣ n) : emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) := by
rw [← geom_sum₂_mul, emultiplicity_mul hp, emultiplicity_eq_zero.2 (not_dvd_geom_sum₂ hp hxy hx hn), zero_add]
