lean_workbook_plus_24949

Proved

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

let $x=ru,y=rv,z=rw$ with $u^2+v^2+w^2=1$ in which $(u,v,w)$ represents an unitary vector meaning direction. then $x^2+y^2+z^2=r^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24949 (x y z r : ℝ) (u v w : ℝ) (h1 : u^2 + v^2 + w^2 = 1) (h2 : x = r * u) (h3 : y = r * v) (h4 : z = r * w) : x^2 + y^2 + z^2 = r^2   :=  by sorry

Source

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

View graph