emultiplicity_pow_prime_sub_pow_prime

English

For primes p and odd p, for x,y ∈ ℤ (or ℕ) with p ∣ x − y and p ∤ x, the LTE formulas hold uniformly across integer and natural contexts; e.g., 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_sub_pow_prime : emultiplicity (↑p) (x ^ p - y ^ p) = emultiplicity (↑p) (x - y) + 1 :=
  by rw [← geom_sum₂_mul, emultiplicity_mul hp, emultiplicity_geom_sum₂_eq_one hp hp1 hxy hx, add_comm]

Похожие утверждения