English
Let p be a prime and a nonnegative integer a. Then for x,y ∈ F (or ℤ) one has v_p(x^{p^a} − y^{p^a}) = v_p(x − y) + a, provided the other standard LTE hypotheses hold (p odd, p | x − y, p ∤ x).
Русский
Пусть p — простое, и a неотрицательное целое. Тогда для x,y выполняется v_p(x^{p^a} − y^{p^a}) = v_p(x − y) + a при выполнении стандартных гипотез LTE (p нечетное, p|x−y, p∤x).
LaTeX
$$For p prime and a ≥ 0, under LTE hypotheses, emultiplicity p (x^{p^a} − y^{p^a}) = emultiplicity p (x − y) + a.$$
Lean4
theorem emultiplicity_geom_sum₂_eq_one : emultiplicity (↑p) (∑ i ∈ range p, x ^ i * y ^ (p - 1 - i)) = 1 :=
by
rw [← Nat.cast_one]
refine emultiplicity_eq_coe.2 ⟨?_, ?_⟩
· rw [pow_one]
exact dvd_geom_sum₂_self hxy
rw [dvd_iff_dvd_of_dvd_sub hxy] at hx
obtain ⟨k, hk⟩ := hxy
rw [one_add_one_eq_two, eq_add_of_sub_eq' hk]
refine mt (dvd_iff_dvd_of_dvd_sub (@odd_sq_dvd_geom_sum₂_sub _ _ y k _ hp1)).mp ?_
rw [pow_two, mul_dvd_mul_iff_left hp.ne_zero]
exact mt hp.dvd_of_dvd_pow hx
