Project-declaredLean 4.31.0
Correctness
KZG.correctness
Plain-language statement
Algebraic correctness of one KZG opening for a coefficient vector.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Source-pinned research
Research proof index
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 filtersView proof record
Project-declaredLean 4.31.0
Mod p eq
KZG.mod_p_eq
Plain-language statement
Powers with exponents congruent modulo p agree in a group of prime order p.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Project-declaredLean 4.31.0
Verify opening equation
KZG.verify_opening_equation
Plain-language statement
Extract the exponent equation enforced by a successful KZG opening verification.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Project-declaredLean 4.31.0
Dist eq min Wt Codewords
LinearCode.dist_eq_minWtCodewords
Plain-language statement
The min distance of a linear code equals the minimum of the weights of non-zero codewords.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Project-declaredLean 4.31.0
Eq span rows
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.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Project-declaredLean 4.31.0
Gen matrix exists
LinearCode.gen_matrix_exists
Plain-language statement
Given a linear code of length ι and dimension dim over a field F, there exists a dim × ι matrix over F which generates the code. Theorem 2.2.7 [GRS25].
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.