Documentation

LeanPool.CCDN.Noether.EulerProductVanishing

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.