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 filtersGuruswamiSudan.card_constraintIndices
Plain-language statement
The indices of constraints are m * (m + 1) / 2.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.card_weigthBoundIndices_eq_sum
Plain-language statement
The number of variables is the sum over j of the number of valid i's.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.coeff_linearCombination_monomial
Plain-language statement
The coefficient of X^i Y^j in a linear combination of monomials is the coefficient of the combination.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.coeff_vec_to_bivariate_coeff
Plain-language statement
Coefficient extraction for coeffVecToBivariate: the (i, j)-coefficient of the bivariate polynomial equals c(i, j) when (i, j) is in the weighted-degree region.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.degree_eval_le_weightedDegree
Plain-language statement
The degree of Q(X, P(X)) is bounded by the (1, k-1)-weighted degree of Q, provided deg(P) ≤ k - 1.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.dvd_eval_of_rootMultiplicity_zero
Plain-language statement
If Q has high multiplicity at (0,0) (meaning all coefficients c_{i,j} with i+j < m are zero) and P(0)=0, then Q(X, P(X)) is divisible by X^m.
Source project: ArkLib
Person-level attribution pending.