forked from Verified-zkEVM/CompPoly
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathCompPoly.lean
More file actions
276 lines (275 loc) · 15 KB
/
Copy pathCompPoly.lean
File metadata and controls
276 lines (275 loc) · 15 KB
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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
module
public import CompPoly.Bivariate.Basic
public import CompPoly.Bivariate.CMvEquiv
public import CompPoly.Bivariate.CoeffRows
public import CompPoly.Bivariate.Deriv
public import CompPoly.Bivariate.Factor
public import CompPoly.Bivariate.FactorMonic
public import CompPoly.Bivariate.GuruswamiSudan
public import CompPoly.Bivariate.GuruswamiSudan.Context
public import CompPoly.Bivariate.GuruswamiSudan.Core
public import CompPoly.Bivariate.GuruswamiSudan.CoreCorrectness
public import CompPoly.Bivariate.GuruswamiSudan.Executable
public import CompPoly.Bivariate.GuruswamiSudan.Filter
public import CompPoly.Bivariate.GuruswamiSudan.FilterCorrectness
public import CompPoly.Bivariate.GuruswamiSudan.Implementations
public import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Basic
public import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Correctness
public import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Dense.Algorithm
public import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Dense.Correctness
public import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan
public import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Algorithm
public import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Basic
public import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness
public import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Basis
public import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Combinations
public import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Common
public import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Completeness
public import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Divisibility
public import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Normalization
public import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Rows
public import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Selection
public import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Soundness
public import CompPoly.Bivariate.GuruswamiSudan.Polynomial
public import CompPoly.Bivariate.GuruswamiSudan.PolynomialCorrectness
public import CompPoly.Bivariate.GuruswamiSudan.Root.Alekhnovich.Algorithm
public import CompPoly.Bivariate.GuruswamiSudan.Root.Alekhnovich.Correctness
public import CompPoly.Bivariate.GuruswamiSudan.Root.Alekhnovich.Lemmas
public import CompPoly.Bivariate.GuruswamiSudan.Root.Common
public import CompPoly.Bivariate.GuruswamiSudan.Root.Common.Lemmas
public import CompPoly.Bivariate.GuruswamiSudan.Root.FieldRoots
public import CompPoly.Bivariate.GuruswamiSudan.Root.FieldRoots.FiniteField
public import CompPoly.Bivariate.GuruswamiSudan.Root.FieldRoots.KoalaBear
public import CompPoly.Bivariate.GuruswamiSudan.Root.RothRuckenstein.Algorithm
public import CompPoly.Bivariate.GuruswamiSudan.Root.RothRuckenstein.Correctness
public import CompPoly.Bivariate.GuruswamiSudan.Root.RothRuckenstein.Lemmas
public import CompPoly.Bivariate.GuruswamiSudan.Root.ShiftedSubstitution
public import CompPoly.Bivariate.GuruswamiSudan.Root.ShiftedSubstitution.Lemmas
public import CompPoly.Bivariate.GuruswamiSudan.Util
public import CompPoly.Bivariate.Kronecker
public import CompPoly.Bivariate.ToPoly
public import CompPoly.Data.Array.Lemmas
public import CompPoly.Data.Classes.DCast
public import CompPoly.Data.Classes.LawfulBEq
public import CompPoly.Data.ExtTreeMap.DTreeMap
public import CompPoly.Data.ExtTreeMap.ExtDTreeMap
public import CompPoly.Data.ExtTreeMap.ExtTreeMap
public import CompPoly.Data.Fin.BigOperators
public import CompPoly.Data.List.Lemmas
public import CompPoly.Data.MvPolynomial.Notation
public import CompPoly.Data.Nat.Bitwise
public import CompPoly.Data.Polynomial.Frobenius
public import CompPoly.Data.Polynomial.MonomialBasis
public import CompPoly.Data.Polynomial.Rabin
public import CompPoly.Data.Polynomial.RabinCertificate
public import CompPoly.Data.RingTheory.AlgebraTower
public import CompPoly.Data.RingTheory.CanonicalEuclideanDomain
public import CompPoly.Data.Vector.Basic
public import CompPoly.Fields.BLS12_377
public import CompPoly.Fields.BLS12_377.Basic
public import CompPoly.Fields.BLS12_377.Fast
public import CompPoly.Fields.BLS12_381
public import CompPoly.Fields.BLS12_381.Basic
public import CompPoly.Fields.BLS12_381.Fast
public import CompPoly.Fields.BN254
public import CompPoly.Fields.BN254.Basic
public import CompPoly.Fields.BN254.Fast
public import CompPoly.Fields.BabyBear
public import CompPoly.Fields.BabyBear.Basic
public import CompPoly.Fields.BabyBear.Ext4
public import CompPoly.Fields.BabyBear.Fast
public import CompPoly.Fields.Basic
public import CompPoly.Fields.Binary.AdditiveNTT.AdditiveNTT
public import CompPoly.Fields.Binary.AdditiveNTT.Algorithm
public import CompPoly.Fields.Binary.AdditiveNTT.Correctness
public import CompPoly.Fields.Binary.AdditiveNTT.Domain
public import CompPoly.Fields.Binary.AdditiveNTT.Impl
public import CompPoly.Fields.Binary.AdditiveNTT.Intermediate
public import CompPoly.Fields.Binary.AdditiveNTT.NovelPolynomialBasis
public import CompPoly.Fields.Binary.BF128Ghash.Basic
public import CompPoly.Fields.Binary.BF128Ghash.Impl
public import CompPoly.Fields.Binary.BF128Ghash.Prelude
public import CompPoly.Fields.Binary.BF128Ghash.XPowTwoPowGcdCertificate
public import CompPoly.Fields.Binary.BF128Ghash.XPowTwoPowModCertificate
public import CompPoly.Fields.Binary.Common
public import CompPoly.Fields.Binary.Tower.Abstract.Algebra
public import CompPoly.Fields.Binary.Tower.Abstract.Basis
public import CompPoly.Fields.Binary.Tower.Abstract.Core
public import CompPoly.Fields.Binary.Tower.Abstract.Split
public import CompPoly.Fields.Binary.Tower.Basic
public import CompPoly.Fields.Binary.Tower.Concrete.Algebra
public import CompPoly.Fields.Binary.Tower.Concrete.Basis
public import CompPoly.Fields.Binary.Tower.Concrete.Core
public import CompPoly.Fields.Binary.Tower.Concrete.Field
public import CompPoly.Fields.Binary.Tower.Equiv
public import CompPoly.Fields.Binary.Tower.Impl
public import CompPoly.Fields.Binary.Tower.Prelude
public import CompPoly.Fields.Binary.Tower.Support.DefiningPoly
public import CompPoly.Fields.Binary.Tower.Support.FinHelpers
public import CompPoly.Fields.Binary.Tower.Support.IrreducibilityAndTraceMapProperty
public import CompPoly.Fields.Binary.Tower.Support.LinearIndependentFin2
public import CompPoly.Fields.Binary.Tower.Support.Preliminaries
public import CompPoly.Fields.Binary.Tower.TensorAlgebra
public import CompPoly.Fields.Extension
public import CompPoly.Fields.Extension.Binomial
public import CompPoly.Fields.Extension.Bridge
public import CompPoly.Fields.Extension.Defs
public import CompPoly.Fields.Extension.Field
public import CompPoly.Fields.Goldilocks
public import CompPoly.Fields.Hachi
public import CompPoly.Fields.Hachi.Ext4
public import CompPoly.Fields.KoalaBear
public import CompPoly.Fields.KoalaBear.Basic
public import CompPoly.Fields.KoalaBear.Ext4
public import CompPoly.Fields.KoalaBear.Ext5
public import CompPoly.Fields.KoalaBear.Ext5.QuinticCertData
public import CompPoly.Fields.KoalaBear.Ext5.QuinticIrreducible
public import CompPoly.Fields.KoalaBear.Ext6
public import CompPoly.Fields.KoalaBear.Ext6.GaloisField
public import CompPoly.Fields.KoalaBear.Ext6.SexticCertData
public import CompPoly.Fields.KoalaBear.Ext6.SexticIrreducible
public import CompPoly.Fields.KoalaBear.Fast
public import CompPoly.Fields.Mersenne
public import CompPoly.Fields.Montgomery.Basic
public import CompPoly.Fields.Montgomery.Native32
public import CompPoly.Fields.Montgomery.Native32Field
public import CompPoly.Fields.Montgomery.Native64x8
public import CompPoly.Fields.Montgomery.Native64x8Defs
public import CompPoly.Fields.Montgomery.Native64x8Field
public import CompPoly.Fields.Montgomery.Native64x8Inv
public import CompPoly.Fields.Montgomery.Native64x8InvDefs
public import CompPoly.Fields.Montgomery.Native64x8Mul
public import CompPoly.Fields.PrattCertificate
public import CompPoly.Fields.Secp256k1
public import CompPoly.LinearAlgebra.Dense
public import CompPoly.LinearAlgebra.Dense.Basic
public import CompPoly.LinearAlgebra.Dense.Kernel
public import CompPoly.LinearAlgebra.Dense.KernelCorrectness
public import CompPoly.LinearAlgebra.Dense.KernelInPlace
public import CompPoly.LinearAlgebra.Dense.KernelInPlaceCorrectness
public import CompPoly.LinearAlgebra.Dense.RowOps
public import CompPoly.LinearAlgebra.Dense.RowOpsCorrectness
public import CompPoly.LinearAlgebra.Dense.RrefSemantics
public import CompPoly.LinearAlgebra.Dense.RrefShape
public import CompPoly.LinearAlgebra.PolynomialMatrix
public import CompPoly.LinearAlgebra.PolynomialMatrix.Basic
public import CompPoly.LinearAlgebra.PolynomialMatrix.Degree
public import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohann
public import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness
public import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Combinations
public import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Conflict
public import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Fast
public import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Leading
public import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.MatrixRows
public import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Measure
public import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Minimal
public import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Reduction
public import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.RowOps
public import CompPoly.LinearAlgebra.PolynomialMatrix.RowSpan
public import CompPoly.LinearAlgebra.PolynomialMatrix.Shifted
public import CompPoly.LinearAlgebra.PolynomialMatrix.ShiftedReduction
public import CompPoly.Multilinear.Basic
public import CompPoly.Multilinear.Equiv
public import CompPoly.Multilinear.ManyEval
public import CompPoly.Multilinear.ManyEval.Basic
public import CompPoly.Multilinear.ManyEval.Correctness
public import CompPoly.Multilinear.TransformEquiv
public import CompPoly.Multivariate.CMvMonomial
public import CompPoly.Multivariate.CMvPolynomial
public import CompPoly.Multivariate.CMvPolynomialEvalLemmas
public import CompPoly.Multivariate.FinSuccEquiv
public import CompPoly.Multivariate.HornerLemmas
public import CompPoly.Multivariate.Lawful
public import CompPoly.Multivariate.MvPolyEquiv
public import CompPoly.Multivariate.MvPolyEquiv.Core
public import CompPoly.Multivariate.MvPolyEquiv.Eval
public import CompPoly.Multivariate.MvPolyEquiv.Instances
public import CompPoly.Multivariate.Operations
public import CompPoly.Multivariate.Rename
public import CompPoly.Multivariate.Restrict
public import CompPoly.Multivariate.Unlawful
public import CompPoly.Multivariate.VarsDegrees
public import CompPoly.Multivariate.Wheels
public import CompPoly.ToMathlib.Finsupp.Fin
public import CompPoly.ToMathlib.MvPolynomial.Equiv
public import CompPoly.ToMathlib.Order.WithBot
public import CompPoly.ToMathlib.Polynomial.BivariateDegree
public import CompPoly.ToMathlib.Polynomial.BivariateEvaluation
public import CompPoly.ToMathlib.Polynomial.BivariateMultiplicity
public import CompPoly.ToMathlib.Polynomial.BivariateWeightedDegree
public import CompPoly.ToMathlib.Polynomial.Div
public import CompPoly.ToMathlib.Polynomial.Irreducible
public import CompPoly.ToMathlib.Polynomial.Roots
public import CompPoly.Univariate.Barycentric
public import CompPoly.Univariate.Basic
public import CompPoly.Univariate.BatchEval
public import CompPoly.Univariate.BatchEval.Context
public import CompPoly.Univariate.BatchEval.Correctness
public import CompPoly.Univariate.BatchEval.Naive
public import CompPoly.Univariate.BatchEval.SubproductTree
public import CompPoly.Univariate.CMvEquiv
public import CompPoly.Univariate.CoefficientInterpolation
public import CompPoly.Univariate.Context
public import CompPoly.Univariate.Deriv
public import CompPoly.Univariate.DivisionCorrectness
public import CompPoly.Univariate.EuclideanAlgorithm
public import CompPoly.Univariate.Lagrange
public import CompPoly.Univariate.LagrangeArray
public import CompPoly.Univariate.Linear
public import CompPoly.Univariate.ManyEval
public import CompPoly.Univariate.ManyEval.Basic
public import CompPoly.Univariate.ManyEval.Correctness
public import CompPoly.Univariate.Modular
public import CompPoly.Univariate.NTT.BabyBear
public import CompPoly.Univariate.NTT.Domain
public import CompPoly.Univariate.NTT.Evaluation
public import CompPoly.Univariate.NTT.FastMul
public import CompPoly.Univariate.NTT.FastMulLow
public import CompPoly.Univariate.NTT.Forward
public import CompPoly.Univariate.NTT.Interpolation
public import CompPoly.Univariate.NTT.Inverse
public import CompPoly.Univariate.NTT.Kernel
public import CompPoly.Univariate.NTT.KoalaBear
public import CompPoly.Univariate.NTT.Transform
public import CompPoly.Univariate.NTTFast.Correctness
public import CompPoly.Univariate.NTTFast.Correctness.Basic
public import CompPoly.Univariate.NTTFast.Correctness.DIF
public import CompPoly.Univariate.NTTFast.Correctness.Pair
public import CompPoly.Univariate.NTTFast.Correctness.Pipeline
public import CompPoly.Univariate.NTTFast.Correctness.Radix4DIF
public import CompPoly.Univariate.NTTFast.Correctness.Radix4DIT
public import CompPoly.Univariate.NTTFast.Evaluation
public import CompPoly.Univariate.NTTFast.FastMul
public import CompPoly.Univariate.NTTFast.FastMulLow
public import CompPoly.Univariate.NTTFast.Interpolation
public import CompPoly.Univariate.NTTFast.Plan
public import CompPoly.Univariate.Quotient.Core
public import CompPoly.Univariate.Quotient.Equiv
public import CompPoly.Univariate.Raw
public import CompPoly.Univariate.Raw.Context
public import CompPoly.Univariate.Raw.Core
public import CompPoly.Univariate.Raw.Division
public import CompPoly.Univariate.Raw.Modular
public import CompPoly.Univariate.Raw.Ops
public import CompPoly.Univariate.Raw.Proofs
public import CompPoly.Univariate.ReedSolomon
public import CompPoly.Univariate.ReedSolomon.GaoCorrectness
public import CompPoly.Univariate.ReedSolomon.GaoDecoder
public import CompPoly.Univariate.ReedSolomon.NTTEncode
public import CompPoly.Univariate.Roots
public import CompPoly.Univariate.Roots.Backend
public import CompPoly.Univariate.Roots.Context
public import CompPoly.Univariate.Roots.Correctness
public import CompPoly.Univariate.Roots.Enumeration
public import CompPoly.Univariate.Roots.Extraction
public import CompPoly.Univariate.Roots.RootProduct
public import CompPoly.Univariate.Roots.SmoothSubgroup
public import CompPoly.Univariate.Roots.SmoothSubgroup.Basic
public import CompPoly.Univariate.Roots.SmoothSubgroup.Correctness
public import CompPoly.Univariate.Roots.Splitter
public import CompPoly.Univariate.ToPoly
public import CompPoly.Univariate.ToPoly.Core
public import CompPoly.Univariate.ToPoly.Degree
public import CompPoly.Univariate.ToPoly.Equiv
public import CompPoly.Univariate.ToPoly.Impl
public import CompPoly.Univariate.Vanishing