Prove2Me

lean_workbook_plus_17171

Proved

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

It is given to make use of the identity- \n (ax+by+cz)2+(ay−bx)2+(bz−cy)2+(cx−az)2=(a2+b2+c2)(x2+y2+z2)(ax + by +cz )^{2} + (ay-bx)^{2} + (bz-cy)^{2} + (cx-az)^{2} = (a^{2} +b^{2}+c^{2})(x^{2} +y^{2}+z^{2})

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_17171 (a b c x y z : ℝ) : (a * x + b * y + c * z) ^ 2 + (a * y - b * x) ^ 2 + (b * z - c * y) ^ 2 + (c * x - a * z) ^ 2 = (a ^ 2 + b ^ 2 + c ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph