Coefficient matrices of rational polynomial families

The coefficient matrix and its expansion are shared by the Zeta5 and Zeta32 changes of polynomial basis.

noncomputable def Zeta5Irrational.coeffMat {h : ℕ} (E : Fin h → Polynomial ℚ) : Matrix (Fin h) (Fin h) ℚ

The coefficient matrix of a family of polynomials.

Equations

• Zeta5Irrational.coeffMat E = Matrix.of fun (a k : Fin h) => (E a).coeff ↑k

theorem Zeta5Irrational.sum_coeffMat {h : ℕ} (E : Fin h → Polynomial ℚ) (hE : ∀ (a : Fin h), (E a).natDegree < h) (a : Fin h) : E a = ∑ k : Fin h, Polynomial.C (coeffMat E a k) * Polynomial.X ^ ↑k