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.zmod_eq_of_srs_power_eq
Plain-language statement
Equality with the second SRS power identifies a field element as the trapdoor.
Source project: ArkLib
Person-level attribution pending.
KZG.correctness
Plain-language statement
Algebraic correctness of one KZG opening for a coefficient vector.
Source project: ArkLib
Person-level attribution pending.
KZG.mod_p_eq
Plain-language statement
Powers with exponents congruent modulo p agree in a group of prime order p.
Source project: ArkLib
Person-level attribution pending.
KZG.verify_opening_equation
Plain-language statement
Extract the exponent equation enforced by a successful KZG opening verification.
Source project: ArkLib
Person-level attribution pending.
LinearCode.dist_eq_minWtCodewords
Plain-language statement
The min distance of a linear code equals the minimum of the weights of non-zero codewords.
Source project: ArkLib
Person-level attribution pending.
LinearCode.eq_span_rows
Plain-language statement
A linear code is equal to the submodule spanned by the rows of the matrix whose rows form a basis of the code.
Source project: ArkLib
Person-level attribution pending.