lean_workbook_plus_70240
ProvedIt is equivalent to \n\n
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_70240 (a b c : ℝ) : a * b ≤ b^2 + a * c ↔ (b - a / 2)^2 + a * (c - a / 4) ≥ 0 := by sorry
Source
It is equivalent to \n\n
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_70240 (a b c : ℝ) : a * b ≤ b^2 + a * c ↔ (b - a / 2)^2 + a * (c - a / 4) ≥ 0 := by sorry