Prove2Me

lean_workbook_plus_76298

Proved

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

From a+bc=b+ca=c+aba+bc=b+ca=c+ab we take that (a−b)(c−1)=0(a-b)(c-1)=0 , (b−c)(a−1)=0(b-c)(a-1)=0 and (c−a)(b−1)=0(c-a)(b-1)=0 .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_76298 {a b c : ℝ} (h : a + b * c = b + c * a ∧ b + c * a = c + a * b) : (a - b) * (c - 1) = 0 ∧ (b - c) * (a - 1) = 0 ∧ (c - a) * (b - 1) = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph