Theorem: book.irrational.lem_aux_i (FormalBook/Chapter_08.lean)

State before:
n : ℕ
x : ℝ
⊢ ∃ c, f_aux n x = ∑ i ∈ Icc n (2 * n), ↑(c i) * x ^ i
Tactic:
sorry
State after:
no goals