Documentation

LeanPool.CCDN.Noether.EulerSparseMatrix

Each row and Euler column uses at most one coefficient of the defining equation, with integer multiplier bounded by its degree.

theorem CCDN.universalEulerMatrix_sparse (k : ℕ) (row : ℕ × ℕ) (col : EulerColumns k) :
universalEulerMatrix k row col = 0 ∨ ∃ (i : EulerLowIndex (k + 2)) (c : ℤ), |c| ≤ ↑(k + 2) ∧ universalEulerMatrix k row col = MvPolynomial.C c * MvPolynomial.X i

An entry is zero or a single coefficient variable with multiplier of absolute value at most the defining equation's degree.