Prove2Me

lean_workbook_plus_50552

Proved

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

Prove that (a−b)5+(b−c)5+(c−a)5\left ( a-b \right )^{5}+\left ( b-c \right )^{5}+\left ( c-a \right )^{5} is divisible by 5(a−b)(b−c)(c−a)5\left ( a-b \right )\left ( b-c \right )\left ( c-a \right ).

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_50552 {a b c : ℤ} : 5 * (a - b) * (b - c) * (c - a) ∣ (a - b)^5 + (b - c)^5 + (c - a)^5   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph