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,483 to 1,488 of 2,569 results.
KZG.CommitmentScheme.choose_s_middle_card
Mathematical statement
chooseSMiddle returns a support set of size n + 1.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.conflict_query_ne_tau
Mathematical statement
A genuine evaluation conflict cannot occur at the hidden trapdoor point.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.correctness
Mathematical statement
The KZG scheme satisfies perfect correctness as defined in CommitmentScheme.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.div_by_monic_zs_to_poly_eq_nodal_erase
Mathematical statement
Dividing the vanishing product by one node gives the erased nodal polynomial.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.filter_map_conflict_length
Mathematical statement
The conflict-branch candidate list contains at least n usable elements.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.filter_map_conflict_nodup
Mathematical statement
The filtered list used by chooseSConflict has no duplicate field elements.
Source project: ArkLib
Person-level attribution pending.