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 filtersJohnsonBound.sum_of_not_equals
Plain-language statement
Counting pairs that disagree at position i in terms of choose_2.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.sum_sum_K_i_eq_n_sub_d
Plain-language statement
Total choose_2 over all coordinates equals choose_2(|B|) · (n - d).
Source project: ArkLib
Person-level attribution pending.
KZG.commit_eq
Plain-language statement
The commitment to a mathlib polynomial poly of maximum degree n is equal to g₁ ^ (poly.1.eval a).val
Source project: ArkLib
Person-level attribution pending.
KZG.commit_eq_c_polynomial
Plain-language statement
The commitment to a computable polynomial (CPolynomial) poly of maximum degree n is equal to g₁ ^ (poly.eval a).val.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.arsdh_game_eq
Plain-language statement
Transition 4: the mapped game equals the ARSDH experiment
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.binding
Plain-language statement
The KZG scheme satisfies evaluation binding provided t-SDH holds.
Source project: ArkLib
Person-level attribution pending.