English
LTE identities extend uniformly to ℤ and ℕ contexts, giving the same v_p(x^n − y^n) = v_p(x − y) + v_p(n) behavior under standard hypotheses.
Русский
LTE свойства распространяются на ℤ и ℕ, давая одинаковое поведение v_p(x^n − y^n) = v_p(x − y) + v_p(n) при стандартных предположениях.
LaTeX
$$Under LTE hypotheses, ∀ p prime, Odd p, ∀ x,y, ∀ 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
iterate 2 rw [← Int.natCast_emultiplicity]
rw [← Int.natCast_dvd_natCast] at hxy hx
push_cast at *
exact Int.emultiplicity_pow_add_pow hp hp1 hxy hx hn
