lean_workbook_plus_9467
ProvedLet . Note that , so is a root of the polynomial. Factoring an out of the polynomial, we have . Note that is a root of the quartic in the factorization, so we can factor an out of the quartic to get . Now, note that is a root of the cubic, so we can once more factor an out of the expression to get . The quadratic is , and thus does not have any real roots, and cannot be factored in the real numbers. Thus, the polynomial is .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_9467 (f : ℝ → ℝ) (h₀ : ∀ x, f x = x^5 + 6 * x^4 + 7 * x^3 - 20 * x^2 - 42 * x - 20) (h₁ : f 2 = 0) : ∀ x, f x = (x - 2) * (x + 1)^2 * (x^2 + 6 * x + 10) := by sorry
Source