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 filtersCoreResults.minWt_ge_of_MDS
Plain-language statement
Every nonzero codeword in a code generated by a k × n MDS matrix has Hamming weight greater or equal to n - k + 1.
Source project: ArkLib
Person-level attribution pending.
CoreResults.vecMul_injective_of_rank_eq
Plain-language statement
If G has full row rank, then every nonzero vector maps to a nonzero codeword.
Source project: ArkLib
Person-level attribution pending.
CWSSStructure.toShape_append
Plain-language statement
The shape induced by appended CWSS data is the generic append of the component shapes.
Source project: ArkLib
Person-level attribution pending.
CWSSStructure.toShape_seqCompose
Plain-language statement
The shape induced by finite sequential CWSS data is the generic sequential composition of the component shapes.
Source project: ArkLib
Person-level attribution pending.
dist_affineCombination_le_dist_interleaved₂
Plain-language statement
Lemma: Distance of Affine Combination is Bounded by Interleaved Distance
Source project: ArkLib
Person-level attribution pending.
dist_interleaved_code_to_code_lb
Plain-language statement
Lemma 4.3, [AHIV22] (row-span lower bound). If the interleaved word U⋆ is more than e far from the interleaved code L^⋈κ, then the row-span of U⋆ contains a word more than e far from L. The additional field-size assumption |F| > e is needed: for small fields one can have a linear subspace of F^ι consisting entirely of e-sparse vector...
Source project: ArkLib
Person-level attribution pending.