lean_workbook_plus_73132

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

squaring again and factorizing we obtain \n $\left( 9\,{x}^{6}-90\,{x}^{5}+431\,{x}^{4}-1100\,{x}^{3}+1927\,{x}^{2}-2394\,x+2241 \right) \left( x-1 \right) ^{2} \geq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_73132 :  ∀ x : ℝ, (9*x^6 - 90*x^5 + 431*x^4 - 1100*x^3 + 1927*x^2 - 2394*x + 2241) * (x - 1)^2 ≥ 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph