lean_workbook_plus_19043

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

prove that for all real numbers $a$ , $b$ , $c$ , and $d$ , $\sqrt{(a^{2}+b^{2})(c^{2}+d^{2})}\geq (ad+bc)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19043 (a b c d : ℝ) : Real.sqrt ((a^2 + b^2) * (c^2 + d^2)) ≥ a * d + b * c   :=  by sorry

Source