z-lean/LinearCodes.lean at main · z-tech/z-lean · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
import LinearCodes.Algebraic.Agreement
import LinearCodes.Algebraic.Code
import LinearCodes.Algebraic.Restriction
import LinearCodes.MCA.Definitions
import LinearCodes.MCA.Properties
import LinearCodes.MCA.SeedProbLemmas
import LinearCodes.MCA.Generators
import LinearCodes.MCA.Lemma53Examples
import LinearCodes.MCA.InducedCode
import LinearCodes.MCA.CAImplications
import LinearCodes.MCA.UniqueDecoding
import LinearCodes.MCA.MaximalDomain
import LinearCodes.MCA.Case2.Counting
import LinearCodes.MCA.Case2.MDSBridge
import LinearCodes.MCA.Case2.Lemma53
import LinearCodes.MCA.Case2Capstone
import LinearCodes.MCA.ConcreteMDS
import LinearCodes.MCA.Tensor
import LinearCodes.MCA.ListDecoding.Core
import LinearCodes.MCA.JohnsonBound
import LinearCodes.MCA.ListDecoding.Witness
import LinearCodes.MCA.ListDecoding.Domains
import LinearCodes.MCA.ListDecoding.Counting
import LinearCodes.MCA.ListDecoding.MCA
import LinearCodes.MCA.Applications.STIR
import LinearCodes.MCA.Applications.Profile
import LinearCodes.LinearCode
import LinearCodes.ReedSolomon
import LinearCodes.ReedSolomonProperties
import LinearCodes.ReedSolomonSoundness
import LinearCodes.MCA.RS.Submodule
import LinearCodes.MCA.RS.ArrayBridge
import LinearCodes.MCA.RS.MCABound