Explicit monomial values of the Euler basis and nonzero minors of the correct Noether order d^2-1.

theorem CCDN.eulerLowBasis_apply {R : Type u_1} [CommRing R] (k : ℕ) (i : EulerLowIndex k) : ↑((eulerLowBasis R k) i) = (MvPolynomial.monomial ↑((Finsupp.degreeLeEquivSym (Fin 2) k).symm i)) 1

The basis vector of eulerLowBasis R k indexed by i is the monomial with exponent vector corresponding to i and coefficient one.

theorem CCDN.eulerTopBasis_apply {R : Type u_1} [CommRing R] (k : ℕ) (i : EulerTopIndex k) : ↑((eulerTopBasis R k) i) = (MvPolynomial.monomial ↑((degreeEqEquivSym (Fin 2) k).symm i)) 1

The basis vector of eulerTopBasis R k indexed by i is the monomial of degree k with exponent vector corresponding to i and coefficient one.

theorem CCDN.exists_eulerClosedForm_nonzero_minor {F : Type u_1} [Field F] [CharZero F] [IsAlgClosed F] (k : ℕ) (f : Polynomial (Polynomial F)) (hf : Irreducible f) (a : F) (ha : a ≠ 0) (hl : f.leadingCoeff = Polynomial.C a) (hdeg : f.natDegree = k + 2) : (eulerClosedFormCoefficientMatrix k f).HasNonzeroMinor ((k + 2) ^ 2 - 1)

A nonzero maximal minor has precisely the universal Noether order d^2-1.