mul_star_dvd_of_aeval_eq_zero_im_ne_zero

English

If p ∈ ℝ[X] and z ∈ ℂ is a non-real root of p with p(z)=0, then X^2 − 2 Re(z) X + |z|^2 divides p.

Русский

Если p ∈ ℝ[X] имеет ненулевой вещественный корень z на комплексной плоскости, то p делится на квадратный множитель X^2 − 2 Re(z) X + |z|^2.

LaTeX

$$$$ X^2 - 2\\operatorname{Re}(z) X + |z|^2 \\mid p(X). $$$$

Lean4

theorem mul_star_dvd_of_aeval_eq_zero_im_ne_zero (p : ℝ[X]) {z : ℂ} (h0 : aeval z p = 0) (hz : z.im ≠ 0) :
    (X - C ((starRingEnd ℂ) z)) * (X - C z) ∣ map (algebraMap ℝ ℂ) p :=
  by
  apply IsCoprime.mul_dvd
  · exact isCoprime_X_sub_C_of_isUnit_sub <| .mk0 _ <| sub_ne_zero.2 <| mt conj_eq_iff_im.1 hz
  · simpa [dvd_iff_isRoot, aeval_conj]
  · simpa [dvd_iff_isRoot]

Похожие утверждения