Euler columns and their coefficient minors commute with every coefficient ring homomorphism, including specialization and reduction in any characteristic.

theorem CCDN.eulerPairCoordinates_basis_left {R : Type u_1} [CommRing R] (k : ℕ) (i : EulerLowIndex k) : (eulerPairCoordinates R k) ((eulerPairBasis R k) (Sum.inl i)) = ((MvPolynomial.monomial ↑((Finsupp.degreeLeEquivSym (Fin 2) k).symm i)) 1, 0)

The basis vector of EulerPairSpace R k from the first low block corresponds to the pair (m, 0) for the associated monomial m of degree at most k.

theorem CCDN.eulerPairCoordinates_basis_right {R : Type u_1} [CommRing R] (k : ℕ) (i : EulerLowIndex k) : (eulerPairCoordinates R k) ((eulerPairBasis R k) (Sum.inr (Sum.inl i))) = (0, (MvPolynomial.monomial ↑((Finsupp.degreeLeEquivSym (Fin 2) k).symm i)) 1)

The basis vector of EulerPairSpace R k from the second low block corresponds to the pair (0, m) for the associated monomial m of degree at most k.

theorem CCDN.eulerPairCoordinates_basis_radial {R : Type u_1} [CommRing R] (k : ℕ) (i : EulerTopIndex k) : (eulerPairCoordinates R k) ((eulerPairBasis R k) (Sum.inr (Sum.inr i))) = (MvPolynomial.X 1 * (MvPolynomial.monomial ↑((degreeEqEquivSym (Fin 2) k).symm i)) 1, -(MvPolynomial.X 0 * (MvPolynomial.monomial ↑((degreeEqEquivSym (Fin 2) k).symm i)) 1))

The basis vector of EulerPairSpace R k from the homogeneous block corresponds to the radial pair (y * m, -(x * m)) for the associated monomial m of degree k.

theorem CCDN.eulerClosedFormCoefficientMatrix_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) (k : ℕ) (f : Polynomial (Polynomial R)) : (eulerClosedFormCoefficientMatrix k f).map ⇑φ = eulerClosedFormCoefficientMatrix k ((bivariateMap φ) f)

The exact-order coefficient matrix specializes entry by entry over any commutative coefficient ring.

theorem CCDN.eulerClosedForm_minor_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) (k r : ℕ) (f : Polynomial (Polynomial R)) (a : Fin r → ℕ × ℕ) (c : Fin r → EulerColumns k) : φ ((eulerClosedFormCoefficientMatrix k f).submatrix a c).det = ((eulerClosedFormCoefficientMatrix k ((bivariateMap φ) f)).submatrix a c).det

Every minor of the Euler closed-form coefficient matrix commutes with applying a coefficient ring homomorphism φ to the equation.