Research proof index

If a non-zero bivariate polynomial f divides a non-zero bivariate polynomial g, then all the coefficients of the quoetient are non-zero. -/ @[grind .] lemma coeff_ne_zero {f q : F[X][Y]} (hg : q * f ≠ 0) : q.coeff ≠ 0 := (ne_zero_iff_coeffs_ne_zero q).1 (quotient_nezero hg) /- If q * f ≠ 0, then the X-degree of q is bounded above by the differen...

There exists a maximal Y-index achieving totalDegree. Above it, total-degree contributions are strictly smaller or the coefficient vanishes.

The total degree of the product of two bivariate polynomials is the sum of their total degrees.

foldingPolynomial in terms of splitNth when q = X ^ n.

If the folding polynomial is zero then so is the original polynomial.

A means to evaluate the original polynomial in terms of the folding polynomial.