Characteristic-independent vanishing on products. A generic integral identity is proved in the fraction field and then specialized; this includes inseparable and repeated factors in every characteristic.
A nonzero Euler kernel vector forces every maximal universal coefficient minor to vanish after specialization.
theorem
CCDN.eulerClosedForm_minor_eq_zero_of_product
{R : Type u_1}
[CommRing R]
(k a b : ℕ)
(ha : 0 < a)
(hb : 0 < b)
(hab : a + b = k + 2)
(g h : Polynomial (Polynomial R))
(hg : bivariateTotalDegree g ≤ a)
(hh : bivariateTotalDegree h ≤ b)
(rows : Fin ((k + 2) ^ 2 - 1) → ℕ × ℕ)
(cols : Fin ((k + 2) ^ 2 - 1) → EulerColumns k)
:
Every maximal Euler minor vanishes on a product with two positive degree budgets, over an arbitrary commutative coefficient ring.