intro h
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
⊢ lamb ∈ primitiveRoots n ℂ → ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1