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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,471 to 1,476 of 2,569 results.
KLDiv_add_le_KLDiv_of_indep
Mathematical statement
If are independent -valued random variables, then
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
KroneckerDelta.generalizedKroneckerDelta_swap
Mathematical 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
Mathematical 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
Mathematical 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.
KZG.CommitmentScheme.arsdh_game_eq
Mathematical statement
Transition 4: the mapped game equals the ARSDH experiment
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.binding
Mathematical statement
The KZG scheme satisfies evaluation binding provided t-SDH holds.
Source project: ArkLib
Person-level attribution pending.