Linearity of μ_X and change of basis in the Hankel determinant

• μX_add, μX_C_mul, μX_sum : μ_X is ℚ-linear in the numerator;
• det_basis_change : for polynomials E a of degree < h, det [μ_X(D_N⁶ E_a E_b / D_K)] = det(C)² Δ_K where C is the coefficient matrix.

theorem Zeta5Irrational.divByMonic_add' {q : Polynomial ℚ} (hq : q.Monic) (P Q : Polynomial ℚ) : (P + Q) /ₘ q = P /ₘ q + Q /ₘ q

theorem Zeta5Irrational.divByMonic_C_mul' {q : Polynomial ℚ} (hq : q.Monic) (c : ℚ) (P : Polynomial ℚ) : Polynomial.C c * P /ₘ q = Polynomial.C c * (P /ₘ q)

theorem Zeta5Irrational.μpoly_add (P Q : Polynomial ℚ) : μpoly (P + Q) = μpoly P + μpoly Q

theorem Zeta5Irrational.μpoly_C_mul (c : ℚ) (P : Polynomial ℚ) : μpoly (Polynomial.C c * P) = c * μpoly P

theorem Zeta5Irrational.μX_add (K : ℕ) (P Q : Polynomial ℚ) : μX K (P + Q) = μX K P + μX K Q

theorem Zeta5Irrational.μX_C_mul (K : ℕ) (c : ℚ) (P : Polynomial ℚ) : μX K (Polynomial.C c * P) = Polynomial.C c * μX K P

theorem Zeta5Irrational.μX_sum {ι : Type u_1} (K : ℕ) (s : Finset ι) (f : ι → Polynomial ℚ) : μX K (∑ i ∈ s, f i) = ∑ i ∈ s, μX K (f i)

theorem Zeta5Irrational.det_basis_change (n : ℕ) (E : Fin (37 * n) → Polynomial ℚ) (hE : ∀ (a : Fin (37 * n)), (E a).natDegree < 37 * n) : (Matrix.of fun (a b : Fin (37 * n)) => μX (40 * n) (D (3 * n) ^ 6 * E a * E b)).det = Polynomial.C ((coeffMat E).det ^ 2) * Δ n

Change of basis.