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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,213 to 1,218 of 2,569 results.
gs_degree_bound_div_lt
Mathematical 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
Mathematical statement
The indices of constraints are m * (m + 1) / 2.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.card_weigthBoundIndices_eq_sum
Mathematical 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
Mathematical 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
Mathematical 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
Mathematical 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.