Theorems · Theorem · field theory

Polynomial.IsMonicOfDegree.eq_isMonicOfDegree_two_mul_isMonicOfDegree

∀ {f : Polynomial ℝ} {n : ℕ},
  f.IsMonicOfDegree (n + 2) → ∃ f₁ f₂, f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

If f : ℝ[X] is monic of degree ≥ 2, then f = f₁ * f₂ with f₁ monic of degree 2 and f₂ monic of degree f.natDegree - 2. This relies on the fact that irreducible polynomials over ℝ have degree at most 2.

Defined in

Mathlib.Analysis.Polynomial.Factorization

Cited by

0 results in Mathlib

Foundations

Depth 298 from the axioms · uses propext, Classical.choice, Quot.sound