English
For any polynomial f ∈ R[X], there exists z ∈ R such that f.eval x − f.eval y = z · (x − y).
Русский
Для любого многочлена f ∈ R[X] существует z ∈ R такое, что f(x) − f(y) = z·(x − y).
LaTeX
$$$\\exists z \\in R, \\; f(x) - f(y) = z \\cdot (x - y) \\text{ with } z = \\sum_i r_i (x^{i}-y^{i})/ (x-y).$$$
Lean4
/-- For any polynomial `f`, `f.eval x - f.eval y` can be expressed as `z * (x - y)`
for some `z` in the ring.
-/
def evalSubFactor (f : R[X]) (x y : R) : { z : R // f.eval x - f.eval y = z * (x - y) } :=
by
refine ⟨f.sum fun i r => r * (powSubPowFactor x y i).val, ?_⟩
delta eval; rw [eval₂_eq_sum, eval₂_eq_sum]
simp only [sum, ← Finset.sum_sub_distrib, Finset.sum_mul]
dsimp
congr with i
rw [mul_assoc, ← (powSubPowFactor x y _).prop, mul_sub]
