lean_workbook_plus_14681
ProvedProve that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14681 (a : ℝ) : a^2 + 2*a + 1 ≥ 8*a - 8*a^2 := by sorry
Source
Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_14681 (a : ℝ) : a^2 + 2*a + 1 ≥ 8*a - 8*a^2 := by sorry