lean_workbook_plus_62541
ProvedProve that for .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_62541 : ∀ a : ℝ, 1/3 ≤ a ∧ a ≤ 1 → (a-1)*(2*a^3 + 2*a^2 + 3*a - 1) ≤ 0 := by sorry
Source
Prove that for .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_62541 : ∀ a : ℝ, 1/3 ≤ a ∧ a ≤ 1 → (a-1)*(2*a^3 + 2*a^2 + 3*a - 1) ≤ 0 := by sorry