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,507 to 1,512 of 2,569 results.
KZG.CommitmentScheme.function_binding_query_eq_tau_branch_maps_to_arsdh
Mathematical statement
The branch that finds a query equal to τ maps to ARSDH.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.h1_zs_eq_h2_prime
Mathematical 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
Mathematical statement
If no degree-n coefficient vector fits the data, interpolation has degree at least n + 1.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.lagrange_zs_conversion
Mathematical statement
Barycentric conversion for interpolation divided by the vanishing polynomial at τ.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.nat_cast_range_card_zmod_of_le
Mathematical statement
Casting the first k ≤ p natural numbers into ZMod p is injective.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.no_data_queryReps_of_function_binding_cond
Mathematical statement
Function-binding failure rules out fitting the deduplicated query representatives.
Source project: ArkLib
Person-level attribution pending.