coefficients of sum a(n) X^n

Stream: Is there code for X?

[Kevin Buzzard]

Do we have this? I need it for LTE and somehow I'm surprised that someone else hasn't run into it already. I will PR if I'm not making a fool of myself :-)

import data.polynomial.degree

variables (R : Type*) [comm_ring R]

open_locale big_operators

open polynomial finset

example (f : ℕ → R) (d : ℕ) (n : ℕ) :
(∑ i in range d, C (f i) * X^i).coeff n = if n < d then f n else 0 :=
begin
  rw finset_sum_coeff,
  split_ifs,
  { suffices : ∀ b, (C (f b) * X ^ b).coeff n = if n = b then f b else 0,
    { simp_rw this,
      simp [h], },
    intro i,
    simp [coeff_X_pow] },
  { refine sum_eq_zero (λ i hi, coeff_eq_zero_of_degree_lt _),
    apply lt_of_le_of_lt (degree_mul_le _ _),
    apply lt_of_le_of_lt (add_le_add (degree_C_le) (degree_X_pow_le i)),
    norm_cast,
    rw finset.mem_range at hi,
    rw [zero_add],
    exact lt_of_lt_of_le hi (le_of_not_lt h), },
end

[Eric Wieser]

That looks like it should be something like docs#finsupp.on_finset_apply

[Eric Wieser]

Oh, on_finset requires f n = 0 for your else clause