Prove2Me

lean_workbook_plus_68948

Proved

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

Prove the equality: ∣z1−z2∣2+∣z2−z3∣2+∣z3−z1∣2+∣z1+z2+z3∣2=3(∣z1∣2+∣z2∣2+∣z3∣2)|z1 - z2|^2 + |z2 - z3|^2 + |z3 - z1|^2 + |z1 + z2 + z3|^2 = 3(|z1|^2 + |z2|^2 + |z3|^2)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_68948 (z1 z2 z3 : ℂ) : ‖z1 - z2‖^2 + ‖z2 - z3‖^2 + ‖z3 - z1‖^2 + ‖z1 + z2 + z3‖^2 = 3 * (‖z1‖^2 + ‖z2‖^2 + ‖z3‖^2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph