lean_workbook_plus_9172
ProvedIt's Cauchy-Schwarz:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_9172 {a b c : ℝ} : (1^2 + 1^2 + 1^2) * (a^2 + b^2 + c^2) ≥ (a + b + c)^2 := by sorrySource
It's Cauchy-Schwarz:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_9172 {a b c : ℝ} : (1^2 + 1^2 + 1^2) * (a^2 + b^2 + c^2) ≥ (a + b + c)^2 := by sorry