lean_workbook_plus_27656
ProvedBy Cauchy's Inequality:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_27656 (a b c : ℝ) : (a^2 + b^2 + c^2 + 2 * a * b) * (4 + 1) ≥ (2 * a + 2 * b + c)^2 := by sorry
Source
By Cauchy's Inequality:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_27656 (a b c : ℝ) : (a^2 + b^2 + c^2 + 2 * a * b) * (4 + 1) ≥ (2 * a + 2 * b + c)^2 := by sorry