lean_workbook_plus_62003

Proved

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

Or, if you don't want to deal with angles, note that the expression $a^2+b^2+c^2+2abc=1,\ (1)$ if treated as quadratic in $a,$ gives you: $a+bc=\sqrt{(1-b^2)(1-c^2)}.$ We get similar expressions if $(1)$ is treated as quadratic in $b$ and $c.$ Multiplying the three expressions we get $(a+bc)(b+ac)(c+ab)=(1-a^2)(1-b^2)(1-c^2).$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_62003 :
  ∀ a b c : ℝ, a^2 + b^2 + c^2 + 2 * a * b * c = 1 → (a + b * c) * (b + a * c) * (c + a * b) = (1 - a^2) * (1 - b^2) * (1 - c^2)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph