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 423 research declarations. Search 10,000 more complete Mathlib declarations.
423 results
Clear filtersdist_row_le_dist_ToInterleavedCode
Plain-language statement
Helper Lemma relating row distance to interleaved distance (as derived from DG25): d((Uᵣ)ᵢ, C) ≤ d^m(Uᵣ, C^m)
Source project: ArkLib
Person-level attribution pending.
DivergenceOfSets.possibleDeltas_subset_relHammingDistRange
Plain-language statement
The set of possible relative Hamming distances between two sets is well-defined.
Source project: ArkLib
Person-level attribution pending.
do_two_uniform_sampling_eq_uniform_prod
Plain-language statement
Proves that a do block sampling two independent uniform distributions is equal to the single uniform distribution over the product type.
Source project: ArkLib
Person-level attribution pending.
Domain.CosetFftDomain.twoNthRoot_correct
Plain-language statement
The value returned by twoNthRoot is a 2 ^ ith root of its input.
Source project: ArkLib
Person-level attribution pending.
Domain.CosetFftDomainClass.card_block_of_mem_subdomain
Plain-language statement
If x lies in the (i + j)th subdomain, then it has exactly 2 ^ j preimages under y ↦ y ^ 2 ^ j from the ith subdomain.
Source project: ArkLib
Person-level attribution pending.
Domain.CosetFftDomainClass.log_right_inverse'
Plain-language statement
Evaluating ω at the index found by log recovers x.
Source project: ArkLib
Person-level attribution pending.