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 16 research declarations. Search 10,000 more complete Mathlib declarations.
16 results
Clear filtersKZG.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.
KZG.CommitmentScheme.function_binding_interpolation_branch_maps_to_arsdh
Plain-language statement
The interpolation branch maps a function-binding violation to ARSDH.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.h1_zs_eq_h2_prime
Plain-language statement
The interpolation-branch output satisfies the ARSDH exponent equation.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.interpolate_degree_ge_of_no_data
Plain-language statement
If no degree-n coefficient vector fits the data, interpolation has degree at least n + 1.
Source project: ArkLib
Person-level attribution pending.