natDegree_le_two — Mathlib

English

If p ∈ ℝ[X] is irreducible, then its natural degree satisfies natDegree(p) ≤ 2.

Русский

Если p ∈ ℝ[X] ирредуцируемый, то натуральная степень p не превосходит 2.

LaTeX

$$$$ \\operatorname{natDegree}(p) \\le 2. $$$$

Lean4

/-- An irreducible real polynomial has natural degree at most two. -/
theorem natDegree_le_two {p : ℝ[X]} (hp : Irreducible p) : natDegree p ≤ 2 :=
  by
  obtain ⟨z, hz⟩ : ∃ z : ℂ, aeval z p = 0 := IsAlgClosed.exists_aeval_eq_zero _ p (degree_pos_of_irreducible hp).ne'
  rw [← finrank_real_complex]
  convert minpoly.natDegree_le z using 1
  · rw [← minpoly.eq_of_irreducible hp hz, natDegree_mul hp.ne_zero (by simpa using hp.ne_zero), natDegree_C, add_zero]
  infer_instance

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