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 filtersKZG.CommitmentScheme.find_query_with_srs_power_success
Plain-language statement
If the SRS-power search returns α, then α satisfies the searched equation.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.find_s_card
Plain-language statement
A successful findS result has cardinality n + 1.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.find_s_existence
Plain-language statement
Some n + 1 subset has interpolation value at τ different from c.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.find_s_subset
Plain-language statement
A successful findS result is a subset of the input set.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.find_s_successful
Plain-language statement
Under the degree hypotheses, findS finds a diverging subset.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.finset_card_gt_of_interpolate_degree_ge
Plain-language statement
A high interpolation degree forces the interpolation set to have more than n + 1 points.
Source project: ArkLib
Person-level attribution pending.