let a := lamb.re
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
⊢ 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
⊢ lamb ∈ primitiveRoots n ℂ → ‖eval (↑q) (X - C lamb)‖ > ↑q - 1