fltp_phi_sq_not_dvd
Provedfltnumber-theoryopen-problemp-adic
If p is an odd prime, p divides a+b, and p does not divide a, then p^2 does not divide Phi_p(a,b) = sum_{i<p} a^i * (-b)^(p-1-i). This is the exact divisibility part of the Lifting-the-Exponent Lemma for the cyclotomic polynomial.
Preamble
import Mathlib.NumberTheory.Multiplicity import Mathlib.Algebra.BigOperators.Group.Finset.Basic
Formal statement
open Finset in
theorem fltp_phi_sq_not_dvd (p : ℕ) [hp : Fact (Nat.Prime p)] (a b : ℤ)
(h_odd : Odd p) (h_dvd : (p : ℤ) ∣ a + b) (h_ndvd : ¬(p : ℤ) ∣ a) :
¬(p : ℤ) ^ 2 ∣ ∑ i ∈ range p, a ^ i * (-b) ^ (p - 1 - i) := by sorrySource