English
Let p be an odd prime and x,y ∈ R with p | x − y and p ∤ x. Then for all n, emultiplicity p (x^n − y^n) = emultiplicity p (x − y) + emultiplicity p n.
Русский
Пусть p — нечетное простое, и x,y в кольце, причём p делит x−y и p не делит x. Тогда для любого n выполняется LTE: v_p(x^n − y^n) = v_p(x − y) + v_p(n).
LaTeX
$$Given p prime and Odd p, with p | (x−y) and p ∤ x, then ∀ n, emultiplicity p (x^n − y^n) = emultiplicity p (x − y) + emultiplicity p n.$$
Lean4
theorem odd_sq_dvd_geom_sum₂_sub (hp : Odd p) :
(p : R) ^ 2 ∣ (∑ i ∈ range p, (a + p * b) ^ i * a ^ (p - 1 - i)) - p * a ^ (p - 1) :=
by
have h1 : ∀ (i : ℕ), (p : R) ^ 2 ∣ (a + ↑p * b) ^ i - (a ^ (i - 1) * (↑p * b) * i + a ^ i) :=
by
intro i
calc
↑p ^ 2 ∣ (↑p * b) ^ 2 := by simp only [mul_pow, dvd_mul_right]
_ ∣ (a + ↑p * b) ^ i - (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i) := by
simp only [sq_dvd_add_pow_sub_sub (↑p * b) a i, ← sub_sub]
simp_rw [← mem_span_singleton, ← Ideal.Quotient.eq] at *
let s : R := (p : R) ^ 2
calc
(Ideal.Quotient.mk (span { s })) (∑ i ∈ range p, (a + (p : R) * b) ^ i * a ^ (p - 1 - i)) =
∑ i ∈ Finset.range p, mk (span { s }) ((a ^ (i - 1) * (↑p * b) * ↑i + a ^ i) * a ^ (p - 1 - i)) :=
by simp_rw [s, RingHom.map_geom_sum₂, ← map_pow, h1, ← map_mul]
_ =
mk (span { s }) (∑ x ∈ Finset.range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
mk (span { s }) (∑ x ∈ Finset.range p, a ^ (x + (p - 1 - x))) :=
by
ring_nf
simp_rw [← map_sum, sum_add_distrib, map_add]
_ =
mk (span { s }) (∑ x ∈ Finset.range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
mk (span { s }) (∑ _x ∈ Finset.range p, a ^ (p - 1)) :=
by
rw [add_right_inj]
have : ∀ (x : ℕ), (hx : x ∈ range p) → a ^ (x + (p - 1 - x)) = a ^ (p - 1) :=
by
intro x hx
rw [← Nat.add_sub_assoc _ x, Nat.add_sub_cancel_left]
exact Nat.le_sub_one_of_lt (Finset.mem_range.mp hx)
rw [Finset.sum_congr rfl this]
_ =
mk (span { s }) (∑ x ∈ Finset.range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
mk (span { s }) (↑p * a ^ (p - 1)) :=
by simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul]
_ = mk (span { s }) (↑p * b * ∑ x ∈ Finset.range p, a ^ (p - 2) * x) + mk (span { s }) (↑p * a ^ (p - 1)) :=
by
simp only [Finset.mul_sum, ← mul_assoc, ← pow_add]
rw [Finset.sum_congr rfl]
rintro (⟨⟩ | ⟨x⟩) hx
· rw [Nat.cast_zero, mul_zero, mul_zero]
· have : x.succ - 1 + (p - 1 - x.succ) = p - 2 :=
by
rw [← Nat.add_sub_assoc (Nat.le_sub_one_of_lt (Finset.mem_range.mp hx))]
exact congr_arg Nat.pred (Nat.add_sub_cancel_left _ _)
rw [this]
ring1
_ = mk (span { s }) (↑p * a ^ (p - 1)) :=
by
have : Finset.sum (range p) (fun (x : ℕ) ↦ (x : R)) = ((Finset.sum (range p) (fun (x : ℕ) ↦ (x : ℕ)))) := by
simp only [Nat.cast_sum]
simp only [add_eq_right, ← Finset.mul_sum, this]
norm_cast
simp only [Finset.sum_range_id]
norm_cast
simp only [Nat.cast_mul, map_mul, Nat.mul_div_assoc p (even_iff_two_dvd.mp (Nat.Odd.sub_odd hp odd_one))]
ring_nf
rw [mul_assoc, mul_assoc]
refine mul_eq_zero_of_left ?_ _
refine Ideal.Quotient.eq_zero_iff_mem.mpr ?_
simp [s, mem_span_singleton]