English
For x,y ∈ ℕ, p prime, with p | x − y and p ∤ x, and odd n, emultiplicity p (x^n − y^n) = emultiplicity p (x − y) + emultiplicity p n; similarly for sums when appropriate parity holds.
Русский
Для x,y ∈ ℕ, простого p с p | x−y и p ∤ x, при нечетном n выполняется LTE для разности; при сумме аналогично.
LaTeX
$$For p prime and 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; similarly for sums when n is odd.$$
Lean4
theorem emultiplicity_pow_sub_pow {x y : ℕ} (hxy : p ∣ x - y) (hx : ¬p ∣ x) (n : ℕ) :
emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n :=
by
obtain hyx | hyx := le_total y x
· iterate 2 rw [← Int.natCast_emultiplicity]
rw [Int.ofNat_sub (Nat.pow_le_pow_left hyx n)]
rw [← Int.natCast_dvd_natCast] at hxy hx
rw [Int.natCast_sub hyx] at *
push_cast at *
exact Int.emultiplicity_pow_sub_pow hp hp1 hxy hx n
·
simp only [Nat.sub_eq_zero_iff_le.mpr (Nat.pow_le_pow_left hyx n), emultiplicity_zero,
Nat.sub_eq_zero_iff_le.mpr hyx, top_add]
