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 16 research declarations. Search 10,000 more complete Mathlib declarations.
16 results
Clear filtersKZG.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.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_s_card
Plain-language statement
A successful findS result has cardinality n + 1.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.find_s_existence
Plain-language statement
Some n + 1 subset has interpolation value at τ different from c.
Source project: ArkLib
Person-level attribution pending.