-
Notifications
You must be signed in to change notification settings - Fork 13
Expand file tree
/
Copy pathCompPoly.lean
More file actions
91 lines (91 loc) · 3.88 KB
/
CompPoly.lean
File metadata and controls
91 lines (91 loc) · 3.88 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
import CompPoly.Bivariate.Basic
import CompPoly.Bivariate.ToPoly
import CompPoly.Data.Array.Lemmas
import CompPoly.Data.Classes.DCast
import CompPoly.Data.Fin.BigOperators
import CompPoly.Data.List.Lemmas
import CompPoly.Data.MvPolynomial.Notation
import CompPoly.Data.Nat.Bitwise
import CompPoly.Data.Polynomial.Frobenius
import CompPoly.Data.Polynomial.MonomialBasis
import CompPoly.Data.RingTheory.AlgebraTower
import CompPoly.Data.RingTheory.CanonicalEuclideanDomain
import CompPoly.Data.Vector.Basic
import CompPoly.Fields.BLS12_377
import CompPoly.Fields.BLS12_381
import CompPoly.Fields.BN254
import CompPoly.Fields.BabyBear
import CompPoly.Fields.Basic
import CompPoly.Fields.Binary.AdditiveNTT.AdditiveNTT
import CompPoly.Fields.Binary.AdditiveNTT.Algorithm
import CompPoly.Fields.Binary.AdditiveNTT.Correctness
import CompPoly.Fields.Binary.AdditiveNTT.Domain
import CompPoly.Fields.Binary.AdditiveNTT.Impl
import CompPoly.Fields.Binary.AdditiveNTT.Intermediate
import CompPoly.Fields.Binary.AdditiveNTT.NovelPolynomialBasis
import CompPoly.Fields.Binary.BF128Ghash.Basic
import CompPoly.Fields.Binary.BF128Ghash.Impl
import CompPoly.Fields.Binary.BF128Ghash.Prelude
import CompPoly.Fields.Binary.BF128Ghash.XPowTwoPowGcdCertificate
import CompPoly.Fields.Binary.BF128Ghash.XPowTwoPowModCertificate
import CompPoly.Fields.Binary.Common
import CompPoly.Fields.Binary.Tower.Abstract.Algebra
import CompPoly.Fields.Binary.Tower.Abstract.Basis
import CompPoly.Fields.Binary.Tower.Abstract.Core
import CompPoly.Fields.Binary.Tower.Abstract.Split
import CompPoly.Fields.Binary.Tower.Basic
import CompPoly.Fields.Binary.Tower.Concrete.Algebra
import CompPoly.Fields.Binary.Tower.Concrete.Basis
import CompPoly.Fields.Binary.Tower.Concrete.Core
import CompPoly.Fields.Binary.Tower.Concrete.Field
import CompPoly.Fields.Binary.Tower.Equiv
import CompPoly.Fields.Binary.Tower.Impl
import CompPoly.Fields.Binary.Tower.Prelude
import CompPoly.Fields.Binary.Tower.Support.DefiningPoly
import CompPoly.Fields.Binary.Tower.Support.FinHelpers
import CompPoly.Fields.Binary.Tower.Support.IrreducibilityAndTraceMapProperty
import CompPoly.Fields.Binary.Tower.Support.LinearIndependentFin2
import CompPoly.Fields.Binary.Tower.Support.Preliminaries
import CompPoly.Fields.Binary.Tower.TensorAlgebra
import CompPoly.Fields.Goldilocks
import CompPoly.Fields.KoalaBear
import CompPoly.Fields.Mersenne
import CompPoly.Fields.PrattCertificate
import CompPoly.Fields.Secp256k1
import CompPoly.Multilinear.Basic
import CompPoly.Multilinear.Equiv
import CompPoly.Multivariate.CMvMonomial
import CompPoly.Multivariate.CMvPolynomial
import CompPoly.Multivariate.CMvPolynomialEvalLemmas
import CompPoly.Multivariate.FinSuccEquiv
import CompPoly.Multivariate.Lawful
import CompPoly.Multivariate.MvPolyEquiv
import CompPoly.Multivariate.MvPolyEquiv.Core
import CompPoly.Multivariate.MvPolyEquiv.Eval
import CompPoly.Multivariate.MvPolyEquiv.Instances
import CompPoly.Multivariate.Operations
import CompPoly.Multivariate.Rename
import CompPoly.Multivariate.Restrict
import CompPoly.Multivariate.Unlawful
import CompPoly.Multivariate.VarsDegrees
import CompPoly.Multivariate.Wheels
import CompPoly.ToMathlib.Finsupp.Fin
import CompPoly.ToMathlib.MvPolynomial.Equiv
import CompPoly.ToMathlib.Polynomial.BivariateDegree
import CompPoly.ToMathlib.Polynomial.BivariateMultiplicity
import CompPoly.ToMathlib.Polynomial.BivariateWeightedDegree
import CompPoly.Univariate.Basic
import CompPoly.Univariate.Lagrange
import CompPoly.Univariate.Linear
import CompPoly.Univariate.Quotient.Core
import CompPoly.Univariate.Quotient.Equiv
import CompPoly.Univariate.Raw
import CompPoly.Univariate.Raw.Core
import CompPoly.Univariate.Raw.Division
import CompPoly.Univariate.Raw.Ops
import CompPoly.Univariate.Raw.Proofs
import CompPoly.Univariate.ToPoly
import CompPoly.Univariate.ToPoly.Core
import CompPoly.Univariate.ToPoly.Degree
import CompPoly.Univariate.ToPoly.Equiv
import CompPoly.Univariate.ToPoly.Impl