lean_workbook_plus_52337
ProvedProve the Cauchy-Schwarz inequality: .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_52337 (m n p q : ℝ) : (m^2 + n^2)*(p^2 + q^2) ≥ (m * p + n * q)^2 := by sorry
Source
Prove the Cauchy-Schwarz inequality: .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_52337 (m n p q : ℝ) : (m^2 + n^2)*(p^2 + q^2) ≥ (m * p + n * q)^2 := by sorry