Exact sparse monomial columns of the Euler differential matrix.

theorem CCDN.bivariatePolynomialEquiv_monomial {R : Type u_1} [CommRing R] (m : Fin 2 →₀ ℕ) (a : R) : (bivariatePolynomialEquiv R) ((MvPolynomial.monomial m) a) = (Polynomial.monomial (m 0)) ((Polynomial.monomial (m 1)) a)

The nested polynomial associated with a monomial in two variables is the nested monomial with outer exponent m 0 and inner exponent m 1.

theorem CCDN.closedFormOperator_monomial_left {R : Type u_1} [CommRing R] (m n s t : ℕ) : (closedFormOperator ((Polynomial.monomial s) ((Polynomial.monomial t) 1))) ((Polynomial.monomial m) ((Polynomial.monomial n) 1), 0) = (Polynomial.monomial (m + s)) ((Polynomial.monomial (n + t - 1)) (↑n - ↑t))

For the monomial equation with outer and inner exponents s and t, the closed-form operator sends the pair (monomial, 0) with exponents m, n to a single monomial with coefficient n - t.

theorem CCDN.closedFormOperator_monomial_right {R : Type u_1} [CommRing R] (m n s t : ℕ) : (closedFormOperator ((Polynomial.monomial s) ((Polynomial.monomial t) 1))) (0, (Polynomial.monomial m) ((Polynomial.monomial n) 1)) = (Polynomial.monomial (m + s - 1)) ((Polynomial.monomial (n + t)) (↑s - ↑m))

For the monomial equation with outer and inner exponents s and t, the closed-form operator sends the pair (0, monomial) with exponents m, n to a single monomial with coefficient s - m.

theorem CCDN.closedFormOperator_monomial_radial {R : Type u_1} [CommRing R] (m n s t : ℕ) : (closedFormOperator ((Polynomial.monomial s) ((Polynomial.monomial t) 1))) ((Polynomial.monomial m) ((Polynomial.monomial (n + 1)) 1), -(Polynomial.monomial (m + 1)) ((Polynomial.monomial n) 1)) = (Polynomial.monomial (m + s)) ((Polynomial.monomial (n + t)) (↑(m + n + 2) - ↑s - ↑t))

The closed-form operator of a monomial equation applied to a radial monomial pair is a single monomial, whose coefficient is the degree of the radial pair's homogeneous factor plus two minus the total degree of the equation.