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 filtersgs_degree_bound_div_lt
Plain-language statement
The GS degree bound with m=1 divided by (k-1) is less than F when |F| ≥ 5 and the RS code is non-degenerate (k+1 ≤ n ≤ F).
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.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.