feat: an irreducible real polynomial has degree ≤2 (#10431)

Mathlib/Analysis/Complex/Polynomial.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Chris Hughes All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Chris Hughes, Junyan Xu
+Authors: Chris Hughes, Junyan Xu, Yury Kudryashov
 -/
 import Mathlib.Algebra.CharZero.Infinite
 import Mathlib.Analysis.Complex.Liouville
@@ -17,11 +17,13 @@ import Mathlib.Topology.Algebra.Polynomial
 This file proves that every nonconstant complex polynomial has a root using Liouville's theorem.
 
 As a consequence, the complex numbers are algebraically closed.
+
+We also show that an irreducible real polynomial has degree at most two.
 -/
 
-open Polynomial Bornology
+open Polynomial Bornology Complex
 
-open scoped Polynomial
+open scoped ComplexConjugate
 
 namespace Complex
 
@@ -46,3 +48,47 @@ instance isAlgClosed : IsAlgClosed ℂ :=
 #align complex.is_alg_closed Complex.isAlgClosed
 
 end Complex
+
+lemma Polynomial.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]
+
+/-- If `z` is a non-real complex root of a real polynomial,
+then `p` is divisible by a quadratic polynomial. -/
+lemma Polynomial.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
+
+/-- An irreducible real polynomial has degree at most two. -/
+lemma Irreducible.degree_le_two {p : ℝ[X]} (hp : Irreducible p) : degree p ≤ 2 := by
+  obtain ⟨z, hz⟩ : ∃ z : ℂ, aeval z p = 0 :=
+    IsAlgClosed.exists_aeval_eq_zero _ p (degree_pos_of_irreducible hp).ne'
+  cases eq_or_ne z.im 0 with
+  | inl hz0 =>
+    lift z to ℝ using hz0
+    erw [aeval_ofReal, IsROrC.ofReal_eq_zero] at hz
+    exact (degree_eq_one_of_irreducible_of_root hp hz).trans_le one_le_two
+  | inr hz0 =>
+    obtain ⟨q, rfl⟩ := p.quadratic_dvd_of_aeval_eq_zero_im_ne_zero hz hz0
+    have hd : degree (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) = 2 := by
+      compute_degree!
+    have hq : IsUnit q := by
+      refine (of_irreducible_mul hp).resolve_left (mt isUnit_iff_degree_eq_zero.1 ?_)
+      rw [hd]
+      exact two_ne_zero
+    refine (degree_mul_le _ _).trans_eq ?_
+    rwa [isUnit_iff_degree_eq_zero.1 hq, add_zero]
+
+/-- An irreducible real polynomial has natural degree at most two. -/
+lemma Irreducible.nat_degree_le_two {p : ℝ[X]} (hp : Irreducible p) : natDegree p ≤ 2 :=
+  natDegree_le_iff_degree_le.2 hp.degree_le_two

Mathlib/Data/IsROrC/Lemmas.lean

@@ -87,3 +87,14 @@ theorem ofRealCLM_norm : ‖(ofRealCLM : ℝ →L[ℝ] K)‖ = 1 :=
 #align is_R_or_C.of_real_clm_norm IsROrC.ofRealCLM_norm
 
 end IsROrC
+
+namespace Polynomial
+
+open ComplexConjugate in
+lemma aeval_conj (p : ℝ[X]) (z : K) : aeval (conj z) p = conj (aeval z p) :=
+  aeval_algHom_apply (IsROrC.conjAe (K := K)) z p
+
+lemma aeval_ofReal (p : ℝ[X]) (x : ℝ) : aeval (IsROrC.ofReal x : K) p = eval x p :=
+  aeval_algHom_apply IsROrC.ofRealAm x p
+
+end Polynomial