Polynomial.ofFn and Polynomial.toFn

In this file we introduce ofFn and toFn, two functions that associate a polynomial to the vector of its coefficients and vice versa. We prove some basic APIs for these functions.

Main definitions

• Polynomial.toFn n associates to a polynomial the vector of its first n coefficients.
• Polynomial.ofFn n associates to a vector of length n the polynomial that has the entries of the vector as coefficients.

noncomputable def Polynomial.toFn {R : Type u_1} [Semiring R] (n : ℕ) : Polynomial R →ₗ[R] Fin n → R

toFn n f is the vector of the first n coefficients of the polynomial f.

Equations

• Polynomial.toFn n = LinearMap.pi fun (i : Fin n) => Polynomial.lcoeff R ↑i

theorem Polynomial.toFn_zero {R : Type u_1} [Semiring R] (n : ℕ) : (toFn n) 0 = 0

def Polynomial.ofFn {R : Type u_1} [Semiring R] [DecidableEq R] (n : ℕ) : (Fin n → R) →ₗ[R] Polynomial R

ofFn n v is the polynomial whose coefficients are the entries of the vector v.

Equations

• Polynomial.ofFn n = { toFun := fun (v : Fin n → R) => { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn v).toFinsupp }, map_add' := ⋯, map_smul' := ⋯ }

theorem Polynomial.ofFn_zero {R : Type u_1} [Semiring R] [DecidableEq R] (n : ℕ) : (ofFn n) 0 = 0

@[simp]

theorem Polynomial.ofFn_zero' {R : Type u_1} [Semiring R] [DecidableEq R] (v : Fin 0 → R) : (ofFn 0) v = 0

theorem Polynomial.ne_zero_of_ofFn_ne_zero {R : Type u_1} [Semiring R] [DecidableEq R] {n : ℕ} {v : Fin n → R} (h : (ofFn n) v ≠ 0) : n ≠ 0

@[simp]

theorem Polynomial.ofFn_coeff_eq_val_of_lt {R : Type u_1} [Semiring R] [DecidableEq R] {n i : ℕ} (v : Fin n → R) (hi : i < n) : ((ofFn n) v).coeff i = v ⟨i, hi⟩

If i < n the i-th coefficient of ofFn n v is v i.

@[simp]

theorem Polynomial.ofFn_coeff_eq_zero_of_ge {R : Type u_1} [Semiring R] [DecidableEq R] {n i : ℕ} (v : Fin n → R) (hi : n ≤ i) : ((ofFn n) v).coeff i = 0

If n ≤ i the i-th coefficient of ofFn n v is 0.

theorem Polynomial.ofFn_natDegree_lt {R : Type u_1} [Semiring R] [DecidableEq R] {n : ℕ} (h : 1 ≤ n) (v : Fin n → R) : ((ofFn n) v).natDegree < n

ofFn n v has natDegree smaller than n.

theorem Polynomial.ofFn_degree_lt {R : Type u_1} [Semiring R] [DecidableEq R] {n : ℕ} (v : Fin n → R) : ((ofFn n) v).degree < ↑n

ofFn n v has degree smaller than n.

theorem Polynomial.ofFn_eq_sum_monomial {R : Type u_1} [Semiring R] [DecidableEq R] {n : ℕ} (v : Fin n → R) : (ofFn n) v = ∑ i : Fin n, (monomial ↑i) (v i)

theorem Polynomial.toFn_comp_ofFn_eq_id {R : Type u_1} [Semiring R] [DecidableEq R] (n : ℕ) (v : Fin n → R) : (toFn n) ((ofFn n) v) = v

theorem Polynomial.injective_ofFn {R : Type u_1} [Semiring R] [DecidableEq R] (n : ℕ) : Function.Injective ⇑(ofFn n)

theorem Polynomial.surjective_toFn {R : Type u_1} [Semiring R] (n : ℕ) : Function.Surjective ⇑(toFn n)

theorem Polynomial.ofFn_comp_toFn_eq_id_of_natDegree_lt {R : Type u_1} [Semiring R] [DecidableEq R] {n : ℕ} {p : Polynomial R} (h_deg : p.natDegree < n) : (ofFn n) ((toFn n) p) = p