simp only [eval_sub, eval_X, eval_C, norm_eq_abs]
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
⊢ ‖eval (↑q) (X - C lamb)‖ ^ 2 = ‖↑q - lamb‖ ^ 2
no goals