lean_workbook_plus_29796

Proved

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

Given that $a, b, c, d$ are real numbers such that $ac-bd=8$ and $ad+bc=6$ , find the value of $(a^{2}+b^{2})(c^{2}+d^{2})$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_29796 (a b c d : ℝ) (h₁ : a * c - b * d = 8) (h₂ : a * d + b * c = 6) : (a^2 + b^2) * (c^2 + d^2) = 100   :=  by sorry

Source