lean_workbook_plus_64142
ProvedLet be a positive integer. Show that for every integer , there exists an integer and a sequence of integers , where (not necessarily dependent on each other) for all integers , such that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_64142 (d S : ℤ) (hd : d > 0) : ∃ n : ℕ, ∃ ε : Fin n → ℤ, ∑ i, ε i * (1 + i * d) ^ 2 = S := by sorry
Source