lean_workbook_plus_12536

Proved

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

(A. Hrabrov) we know that $(a^2+d^2)(c^2+b^2) = (ab+cd)^2 + (ac-bd)^2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_12536 {a b c d : ℝ} : (a ^ 2 + d ^ 2) * (c ^ 2 + b ^ 2) = (a * b + c * d) ^ 2 + (a * c - b * d) ^ 2   :=  by sorry

Source