lean_workbook_plus_81246

Proved

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

$(a^2+b^2+c^2)(\frac{1}{bc}+\frac{1}{ca}+\frac{1}{ab}) = \frac{a^2}{bc}+\frac{b^2}{ca}+\frac{c^2}{ab}+\frac{a}{b}+\frac{b}{a}+\frac{b}{c}+\frac{c}{b}+\frac{c}{a}+\frac{a}{c}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81246 (a b c : ℝ) : (a^2+b^2+c^2)*(1/(b*c) + 1/(c*a) + 1/(a*b)) = a^2/(b*c) + b^2/(c*a) + c^2/(a*b) + a/b + b/a + b/c + c/b + c/a + a/c   :=  by sorry

Source

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

View graph