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 573 research declarations. Search 10,000 more complete Mathlib declarations.
573 results
Clear filtersPolynomial.Bivariate.totalDegree_mul
Plain-language statement
The total degree of the product of two bivariate polynomials is the sum of their total degrees.
Source project: ArkLib
Person-level attribution pending.
Polynomial.folding_polynomial_eq_sum_splitNth
Plain-language statement
foldingPolynomial in terms of splitNth when q = X ^ n.
Source project: ArkLib
Person-level attribution pending.
Polynomial.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.