Lean-Workbook Plus 71078: A polynomial with nonpositive coefficients is nonpositive

Proved

WorkbookRestored.plus_71078

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

If every coefficient of a real polynomial $P$ is nonpositive, then $P(x)\le0$ for every $x\ge0$ .

Source: Lean-Workbook row lean_workbook_plus_71078 (Apache-2.0), original record. This repair only restores required imports and namespaces; the mathematical declaration is unchanged.

Preamble

import Mathlib.Algebra.Polynomial.Eval.Degree
import Mathlib.Data.Real.Basic

Formal statement

theorem WorkbookRestored.plus_71078 (P : Polynomial ℝ) (hP : ∀ n, P.coeff n ≤ 0) (x : ℝ) (hx : 0 ≤ x) : P.eval x ≤ 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_71078; immutable original Prove2Me node d22585c9-4e0b-4875-9f59-8d1f5367afd6

View graph