Documentation
ArkLib
.
Data
.
CodingTheory
.
ProximityGap
.
BCIKS20
.
Prelude
Search
return to top
source
Imports
Init
Mathlib.LinearAlgebra.Vandermonde
Mathlib.Tactic.ComputeDegree
ArkLib.Data.CodingTheory.InterleavedCode
ArkLib.Data.CodingTheory.PolishchukSpielman
ArkLib.Data.Polynomial.Trivariate
ArkLib.Data.Probability.Instances
Mathlib.Algebra.BigOperators.Fin
Mathlib.Algebra.Polynomial.Basic
Mathlib.Algebra.Polynomial.BigOperators
Mathlib.Algebra.Polynomial.Coeff
Mathlib.Algebra.Polynomial.Roots
Mathlib.Data.Fin.SuccPred
Mathlib.Data.Finset.Card
Mathlib.Data.Finset.Preimage
Mathlib.Data.Fintype.BigOperators
Mathlib.Data.Fintype.Card
Mathlib.Data.Fintype.EquivFin
Mathlib.Data.Fintype.Fin
Mathlib.Data.Matrix.Basic
Mathlib.Data.Matrix.Block
Mathlib.Data.Matrix.Mul
Mathlib.Data.Nat.Find
Mathlib.LinearAlgebra.Matrix.Adjugate
Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Mathlib.LinearAlgebra.Matrix.Polynomial
Mathlib.LinearAlgebra.Matrix.Rank
Mathlib.LinearAlgebra.Matrix.RowCol
Mathlib.LinearAlgebra.Matrix.SchurComplement
Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Mathlib.Logic.Function.Basic
Mathlib.Probability.ProbabilityMassFunction.Monad
ArkLib.Data.CodingTheory.BerlekampWelch.BerlekampWelch
ArkLib.Data.CodingTheory.PolishchukSpielman.Degrees
ArkLib.Data.CodingTheory.ProximityGap.Basic
Mathlib.Algebra.GroupWithZero.Units.Basic
Mathlib.Algebra.Order.BigOperators.Expect
Mathlib.Algebra.Polynomial.Degree.Lemmas
Mathlib.Algebra.Polynomial.Degree.Operations
Mathlib.Algebra.Polynomial.Degree.SmallDegree
Mathlib.Algebra.Polynomial.Degree.Units
Mathlib.Data.Fin.Tuple.Basic
Mathlib.Data.Fin.Tuple.Embedding
Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Mathlib.Logic.Equiv.Fin.Basic
Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Mathlib.Algebra.BigOperators.Group.Finset.Basic
Imported by