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

State before:
p : ℕ
h_p : p ≠ 2
inst✝² : Fact p.Prime
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
⊢ ∃ ζ, ∀ (α : Kˣ), ∃ k, α = ζ ^ k
Tactic:
sorry
State after:
no goals