Recovering a polynomial of bounded degree from its coefficient vector

Polynomial.ofFn n and Polynomial.toFn n pass between vectors of length n and polynomials. Mathlib records that a polynomial of natDegree below n is recovered from its first n coefficients; this file states the same recovery in terms of degree, so that it also applies to the zero polynomial. This file also records evaluation of the coefficient vector and reconstruction of a coordinate vector as a power of X.

@[simp]

theorem Polynomial.toFn_apply {R : Type u_1} [Semiring R] (n : ℕ) (p : Polynomial R) (i : Fin n) : (toFn n) p i = p.coeff ↑i

Evaluating the coefficient vector reads the corresponding polynomial coefficient.

@[simp]

theorem Polynomial.ofFn_single {R : Type u_1} [Semiring R] [DecidableEq R] {n : ℕ} (l : Fin n) : ((ofFn n) fun (i : Fin n) => if i = l then 1 else 0) = X ^ ↑l

The coordinate vector with value one at l reconstructs the monomial X ^ l.val.

theorem Polynomial.ofFn_comp_toFn_eq_id_of_degree_lt {R : Type u_1} [Semiring R] [DecidableEq R] {n : ℕ} {p : Polynomial R} (h : p.degree < ↑n) : (ofFn n) ((toFn n) p) = p

A polynomial of degree below n is recovered from its vector of first n coefficients. This is the degree form of Polynomial.ofFn_comp_toFn_eq_id_of_natDegree_lt, which also covers the zero polynomial.