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 573 research declarations. Search 10,000 more complete Mathlib declarations.
573 results
Clear filtersLinearCode.gen_matrix_exists
Plain-language statement
Given a linear code of length ι and dimension dim over a field F, there exists a dim × ι matrix over F which generates the code. Theorem 2.2.7 [GRS25].
Source project: ArkLib
Person-level attribution pending.
LinearCode.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.