Prove2Me

lean_workbook_plus_36704

Proved

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

If ab−c+bc−a+ca−b=0 \frac {a}{b - c } + \frac {b}{c - a } + \frac {c}{a - b } = 0 , prove that a(b−c)2 \frac {a}{(b - c)^2 } + b(c−a)2 \frac {b}{(c - a)^2 } + c(a−b)2=0 \frac {c}{(a - b)^2 } = 0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_36704 (a b c : ℝ) (hab : a ≠ b) (hbc : b ≠ c) (hca : c ≠ a) : (a / (b - c) + b / (c - a) + c / (a - b) = 0) → (a / (b - c) ^ 2 + b / (c - a) ^ 2 + c / (a - b) ^ 2 = 0)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph