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 423 research declarations. Search 10,000 more complete Mathlib declarations.
423 results
Clear filtersPolynomial.FoldingPolynomial.polyFold_natDegree_le
Plain-language statement
The degree bound of polyFold in terms of the degree of the original polynomial and k.
Source project: ArkLib
Person-level attribution pending.
Polynomial.FoldingPolynomial.polyFold_step
Plain-language statement
Recursive case of polyFold: when 0 < k ≤ f.natDegree, polyFold f k r = C ((f %ₘ X^k).eval r) + X * polyFold (f /ₘ X^k) k r.
Source project: ArkLib
Person-level attribution pending.
Polynomial.indicator_eq_1_of_neg_empty_empty_of_pos_nonempty
Plain-language statement
The indicator polynomial is a constant one polynomial if the set neg is empty while pos is not.
Source project: ArkLib
Person-level attribution pending.
Polynomial.indicator_eq_1_on_pos
Plain-language statement
Indicator evaluated on an element of pos is equal to 1.
Source project: ArkLib
Person-level attribution pending.
Polynomial.indicator_ne_zero_of_pos_nonempty
Plain-language statement
If pos is non-empty then the indicator polynomial is the constant zero polynomial.
Source project: ArkLib
Person-level attribution pending.
Polynomial.splitNth_of_sum_comp
Plain-language statement
splitNth is the left inverse of the n-way recombination: splitting the polynomial ∑ j, X^j * (u j)(X^n) recovers u i for each component i.
Source project: ArkLib
Person-level attribution pending.