lean_workbook_plus_29341

Open

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

If $P(x) \in \mathbb{Z}[x]$ , then for every two distinct integers $a,b$ we have that $a-b | P(a) - P(b)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_29341 (P : Polynomial ℤ) {a b : ℤ} (h : a ≠ b) : a - b ∣ P.eval a - P.eval b   :=  by sorry

Source