English
For a real polynomial p ∈ ℝ[X], if z ∈ ℂ is a non-real root with p(z) = 0, then X^2 − C (2 z.re) X + C(|z|^2) divides p.
Русский
Для реального многочлена p, если z ∈ ℂ − ℝ является ненулевым корнем, то X^2 − 2 Re(z) X + |z|^2 делит p.
LaTeX
$$$$ X^2 - 2\\operatorname{Re}(z) X + |z|^2 \\mid p(X). $$$$
Lean4
/-- If `z` is a non-real complex root of a real polynomial,
then `p` is divisible by a quadratic polynomial. -/
theorem quadratic_dvd_of_aeval_eq_zero_im_ne_zero (p : ℝ[X]) {z : ℂ} (h0 : aeval z p = 0) (hz : z.im ≠ 0) :
X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2) ∣ p :=
by
rw [← map_dvd_map' (algebraMap ℝ ℂ)]
convert p.mul_star_dvd_of_aeval_eq_zero_im_ne_zero h0 hz
calc
map (algebraMap ℝ ℂ) (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2))
_ = X ^ 2 - C (↑(2 * z.re) : ℂ) * X + C (‖z‖ ^ 2 : ℂ) := by simp
_ = (X - C (conj z)) * (X - C z) :=
by
rw [← add_conj, map_add, ← mul_conj', map_mul]
ring
