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,477 to 1,482 of 2,569 results.
KZG.CommitmentScheme.binding_cond_le_t_sdh_cond
Mathematical statement
Transition 2: a successful extended binding run maps to a successful t-SDH instance.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.binding_game_ext_eq_binding_game
Mathematical statement
Transition 1: extending the binding game output preserves the event.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.choose_s_conflict_alpha
Mathematical statement
The conflict point is not already included in chooseSConflict.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.choose_s_conflict_insert_eval_ne_zero
Mathematical statement
The conflict-branch adjoined vanishing product is nonzero at τ.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.choose_s_conflict_size
Mathematical statement
chooseSConflict returns exactly n elements.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.choose_s_conflict_tau
Mathematical statement
The trapdoor τ is not in the conflict-branch support set.
Source project: ArkLib
Person-level attribution pending.