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 573 research declarations. Search 10,000 more complete Mathlib declarations.
573 results
Clear filtersKZG.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.
KZG.CommitmentScheme.find_a_card
Plain-language statement
A successful findA result has cardinality n + 1.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.find_a_subset
Plain-language statement
A successful findA result is a subset of the search universe.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.find_a_successful
Plain-language statement
If the interpolation over U has degree at least n, then findA succeeds.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.find_conflict_successful
Plain-language statement
If findConflict returns a pair, that pair has equal queries and distinct responses.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.find_conflict_unsuccessful
Plain-language statement
If findConflict returns none, no pair of indices has equal query and unequal response.
Source project: ArkLib
Person-level attribution pending.