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 559 to 564 of 2,569 results.
CoPset.coPsetRaw_eq
Mathematical statement
Two CoPsetRaw trees are equal if they have the same membership function and both are well-formed.
Source project: Iris-Lean
Person-level attribution pending.
CoreDefinitions.TensorGenerator_eq_TensorGenerator_Explicit
Mathematical statement
The tensor product generator TensorGenerator and the explicit componentwise generator TensorGenerator_Explicit agree under the canonical isomorphism between F^ℓ ⊗ F^ℓ′ and (ℓ × ℓ') → F.
Source project: ArkLib
Person-level attribution pending.
CoreResults.colRank_genMatrix_eq_dim_of_MDS
Mathematical statement
A linear code LC of length ι and dimension dim over a field F is MDS if any dim columns of the generator matrix whose rows are an F-basis of LC are linearly independent.[GRS25] Equivalently, a linear code is MDS if and only if its generator matrix is MDS. Note: the hypothesis 0 < dim LC is necessary because for a trivial code (dim = 0),...
Source project: ArkLib
Person-level attribution pending.
CoreResults.IsMDS_of_matrix_IsMDS
Mathematical statement
If a generator matrix is MDS with at least one row, then the code it generates is MDS.
Source project: ArkLib
Person-level attribution pending.
CoreResults.matrix_IsMDS_of_IsMDS
Mathematical statement
If a linear code generated by a full-rank matrix is MDS, then the matrix is MDS.
Source project: ArkLib
Person-level attribution pending.
CoreResults.minWt_ge_of_MDS
Mathematical 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.