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 187 research declarations. Search 10,000 more complete Mathlib declarations.
187 results
Clear filtersJohnsonBound.johnson_condition_strong_implies_2_le_B_card
Plain-language statement
The strong Johnson condition forces the code to have at least two codewords.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.johnson_condition_weak_implies_strong
Plain-language statement
The weak Johnson condition implies the strong one on the ball intersection.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.sqrt_le_J
Plain-language statement
The binary Johnson bound 1 - √(1-δ) is at most the q-ary bound J q δ.
Source project: ArkLib
Person-level attribution pending.
KroneckerDelta.generalizedKroneckerDelta_swap
Plain-language statement
Swapping two of the upper indices of the generalized Kronecker delta negates it. This is one row transposition of the underlying determinant.
Source project: Physlib
Person-level attribution pending.
KZG.commit_eq
Plain-language statement
The commitment to a mathlib polynomial poly of maximum degree n is equal to g₁ ^ (poly.1.eval a).val
Source project: ArkLib
Person-level attribution pending.
KZG.commit_eq_c_polynomial
Plain-language statement
The commitment to a computable polynomial (CPolynomial) poly of maximum degree n is equal to g₁ ^ (poly.eval a).val.
Source project: ArkLib
Person-level attribution pending.