rwa [this]
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this✝ : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
this : ∑ j ∈ range p, f1k₂ a j • ζ ^ j = ↑a - ↑a * ζ ^ 2
⊢ ↑↑p ∣ ∑ j ∈ range p, f1k₂ a j • ζ ^ j
no goals