Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 10 research declarations. Search 10,000 more complete Mathlib declarations.
10 results
Clear filtersPolynomial.FoldingPolynomial.eq_zero_of_folding_polynomial_eq_zero
Plain-language statement
If the folding polynomial is zero then so is the original polynomial.
Source project: ArkLib
Person-level attribution pending.
Polynomial.FoldingPolynomial.eval_property_of_folding_polynomial
Plain-language statement
A means to evaluate the original polynomial in terms of the folding polynomial.
Source project: ArkLib
Person-level attribution pending.
Polynomial.FoldingPolynomial.folded_poly_degree_bound
Plain-language statement
If we fold a polynomial using a folding polynomial Q with appropriate degree bounds in each variable we get a univariate polynomial with a degree bound.
Source project: ArkLib
Person-level attribution pending.
Polynomial.FoldingPolynomial.folding_polynomial_deg_x
Plain-language statement
The degree of the foldingPolynomial q f is precisely f.natDegree / q.natDegree in the first variable.
Source project: ArkLib
Person-level attribution pending.
Polynomial.FoldingPolynomial.folding_polynomial_deg_y_bound
Plain-language statement
The degree of foldingPolynomial is less than q.degree in the second variable, when q is not a constant polynomial.
Source project: ArkLib
Person-level attribution pending.
Polynomial.FoldingPolynomial.folding_polynomial_is_unique
Plain-language statement
The uniqueness of the folding polynomial.
Source project: ArkLib
Person-level attribution pending.