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 filtersKZG.CommitmentScheme.choose_s_middle_card
Plain-language statement
chooseSMiddle returns a support set of size n + 1.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.conflict_query_ne_tau
Plain-language statement
A genuine evaluation conflict cannot occur at the hidden trapdoor point.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.correctness
Plain-language 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
Plain-language 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
Plain-language 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
Plain-language statement
The filtered list used by chooseSConflict has no duplicate field elements.
Source project: ArkLib
Person-level attribution pending.