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 filtersLinearCode.projectedCode_linearCombination
Plain-language statement
Let T be a finite subset of ι. If every word in a collection lies in the projected code C|[T], then so do all F-linear combinations of these.
Source project: ArkLib
Person-level attribution pending.
LinearCode.singleton_bound_linear
Plain-language statement
Singleton bound for linear codes
Source project: ArkLib
Person-level attribution pending.
LinearCombination.linearCombination_ne_zero
Plain-language statement
A nonzero linear combination of linearly independent vectors is nonzero.
Source project: ArkLib
Person-level attribution pending.
LinearMvExtension.powContraction_is_right_inverse_to_linearMvExtension
Project documentation
The Semiring morphism that maps m-variate polynomials onto univariate polynomials by evaluating them at (X^(2⁰), ... , X^(2ᵐ⁻¹)), i.e. sending aₑ X₀^σ(0) ⬝ ⋯ ⬝ Xₘ₋₁^σ(m-1) → aₑ (X^(2⁰))^σ(0) ⬝ ⋯ ⬝ (X^(2ᵐ⁻¹))^σ(m-1) for all σ : Fin m → ℕ -/ def powAlgHom : MvPolynomial (Fin m) F →ₐ[F] Polynomial F := aeval fun j => Polynomial.X ^ (2 ^ (j : ℕ)) lemma...
Source project: ArkLib
Person-level attribution pending.
LinearTransformations.isMCA_projectedGenerator_of_isMCA
Plain-language statement
If the MCA condition IsMCA holds for a projected generator, then IsMCA holds for the original generator G with the zero-extension defined above.
Source project: ArkLib
Person-level attribution pending.
Matrix.full_row_rank_via_rank_subLeftFull
Plain-language statement
An m×n matrix has full rank if the submatrix consisting of columns 1 through m has rank m.
Source project: ArkLib
Person-level attribution pending.