English
For x,y ∈ ℤ and prime p with p ∣ x + y and p ∤ x, if n is odd, then emultiplicity p (x^n + y^n) = emultiplicity p (x + y) + emultiplicity p n.
Русский
Для x,y ∈ ℤ и простого p с p | x + y и p ∤ x, при нечетном n выполняется emultiplicity p (x^n + y^n) = emultiplicity p (x + y) + emultiplicity p n.
LaTeX
$$For p prime, Odd p, ∀ x,y ∈ ℤ, if p | (x + y) and p ∤ x, ∀ n with Odd n, emultiplicity p (x^n + y^n) = emultiplicity p (x + y) + emultiplicity p n.$$
Lean4
theorem emultiplicity_pow_add_pow {x y : ℤ} (hxy : ↑p ∣ x + y) (hx : ¬↑p ∣ x) {n : ℕ} (hn : Odd n) :
emultiplicity (↑p) (x ^ n + y ^ n) = emultiplicity (↑p) (x + y) + emultiplicity p n :=
by
rw [← sub_neg_eq_add] at hxy
rw [← sub_neg_eq_add, ← sub_neg_eq_add, ← Odd.neg_pow hn]
exact Int.emultiplicity_pow_sub_pow hp hp1 hxy hx n
