Theorem: book.quadratic_reciprocity.fact_B (FormalBook/Chapter_05.lean)

State before:
p✝ : ℕ
h_p : p✝ ≠ 2
inst✝² : Fact p✝.Prime
p : ℕ
inst✝¹ : Fact (Prime p)
K : Type u_1
inst✝ : Field K
ζ : Kˣ
h_1 : ζ ^ p = 1
h_2 : ζ ≠ 1
⊢ X ^ (p - 1) - 1 = ∏ i ∈ Icc 1 p, (X - Polynomial.C ↑ζ ^ i)
Tactic:
sorry
State after:
no goals