lean_workbook_plus_68219

Proved

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

Prove that, $(x-y)^{5}+(y-z)^{5}+(z-x)^{5}$ is divisible by $5(x-y)(y-z)(z-x)$ , where $x,y$ and $z$ are integers, that are not equal in pairs.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_68219 {x y z : ℤ} (hx : x ≠ y) (hy : y ≠ z) (hz : z ≠ x) : 5 * (x - y) * (y - z) * (z - x) ∣ (x - y) ^ 5 + (y - z) ^ 5 + (z - x) ^ 5   :=  by sorry

Source

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

View graph