lean_workbook_plus_9793
Provedprove that,
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_9793 (a b c d : ℝ) : Real.sqrt ((a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2)) ≥ a * c + b * d := by sorry
Source
prove that,
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_9793 (a b c d : ℝ) : Real.sqrt ((a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2)) ≥ a * c + b * d := by sorry