CompPoly.lean

import CompPoly.Bivariate.Basic
import CompPoly.Bivariate.CMvEquiv
import CompPoly.Bivariate.CoeffRows
import CompPoly.Bivariate.Deriv
import CompPoly.Bivariate.Factor
import CompPoly.Bivariate.FactorMonic
import CompPoly.Bivariate.GuruswamiSudan
import CompPoly.Bivariate.GuruswamiSudan.Context
import CompPoly.Bivariate.GuruswamiSudan.Core
import CompPoly.Bivariate.GuruswamiSudan.CoreCorrectness
import CompPoly.Bivariate.GuruswamiSudan.Executable
import CompPoly.Bivariate.GuruswamiSudan.Filter
import CompPoly.Bivariate.GuruswamiSudan.FilterCorrectness
import CompPoly.Bivariate.GuruswamiSudan.Implementations
import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Basic
import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Correctness
import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Dense.Algorithm
import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Dense.Correctness
import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan
import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Algorithm
import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Basic
import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness
import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Basis
import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Combinations
import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Common
import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Completeness
import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Divisibility
import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Normalization
import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Rows
import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Selection
import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Soundness
import CompPoly.Bivariate.GuruswamiSudan.Polynomial
import CompPoly.Bivariate.GuruswamiSudan.PolynomialCorrectness
import CompPoly.Bivariate.GuruswamiSudan.Root.Alekhnovich.Algorithm
import CompPoly.Bivariate.GuruswamiSudan.Root.Alekhnovich.Correctness
import CompPoly.Bivariate.GuruswamiSudan.Root.Alekhnovich.Lemmas
import CompPoly.Bivariate.GuruswamiSudan.Root.Common
import CompPoly.Bivariate.GuruswamiSudan.Root.Common.Lemmas
import CompPoly.Bivariate.GuruswamiSudan.Root.FieldRoots
import CompPoly.Bivariate.GuruswamiSudan.Root.FieldRoots.FiniteField
import CompPoly.Bivariate.GuruswamiSudan.Root.FieldRoots.KoalaBear
import CompPoly.Bivariate.GuruswamiSudan.Root.RothRuckenstein.Algorithm
import CompPoly.Bivariate.GuruswamiSudan.Root.RothRuckenstein.Correctness
import CompPoly.Bivariate.GuruswamiSudan.Root.RothRuckenstein.Lemmas
import CompPoly.Bivariate.GuruswamiSudan.Root.ShiftedSubstitution
import CompPoly.Bivariate.GuruswamiSudan.Root.ShiftedSubstitution.Lemmas
import CompPoly.Bivariate.GuruswamiSudan.Util
import CompPoly.Bivariate.Kronecker
import CompPoly.Bivariate.ToPoly
import CompPoly.Data.Array.Lemmas
import CompPoly.Data.Classes.DCast
import CompPoly.Data.Classes.LawfulBEq
import CompPoly.Data.ExtTreeMap.DTreeMap
import CompPoly.Data.ExtTreeMap.ExtDTreeMap
import CompPoly.Data.ExtTreeMap.ExtTreeMap
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.KoalaBear.Basic
import CompPoly.Fields.KoalaBear.Fast
import CompPoly.Fields.Mersenne
import CompPoly.Fields.PrattCertificate
import CompPoly.Fields.Secp256k1
import CompPoly.LinearAlgebra.Dense
import CompPoly.LinearAlgebra.Dense.Basic
import CompPoly.LinearAlgebra.Dense.Kernel
import CompPoly.LinearAlgebra.Dense.KernelCorrectness
import CompPoly.LinearAlgebra.Dense.RowOps
import CompPoly.LinearAlgebra.Dense.RowOpsCorrectness
import CompPoly.LinearAlgebra.Dense.RrefSemantics
import CompPoly.LinearAlgebra.Dense.RrefShape
import CompPoly.LinearAlgebra.PolynomialMatrix
import CompPoly.LinearAlgebra.PolynomialMatrix.Basic
import CompPoly.LinearAlgebra.PolynomialMatrix.Degree
import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohann
import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness
import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Combinations
import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Conflict
import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Fast
import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Leading
import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.MatrixRows
import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Measure
import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Minimal
import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Reduction
import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.RowOps
import CompPoly.LinearAlgebra.PolynomialMatrix.RowSpan
import CompPoly.LinearAlgebra.PolynomialMatrix.Shifted
import CompPoly.LinearAlgebra.PolynomialMatrix.ShiftedReduction
import CompPoly.Multilinear.Basic
import CompPoly.Multilinear.Equiv
import CompPoly.Multilinear.ManyEval
import CompPoly.Multilinear.ManyEval.Basic
import CompPoly.Multilinear.ManyEval.Correctness
import CompPoly.Multilinear.TransformEquiv
import CompPoly.Multivariate.CMvMonomial
import CompPoly.Multivariate.CMvPolynomial
import CompPoly.Multivariate.CMvPolynomialEvalLemmas
import CompPoly.Multivariate.FinSuccEquiv
import CompPoly.Multivariate.HornerLemmas
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.BivariateEvaluation
import CompPoly.ToMathlib.Polynomial.BivariateMultiplicity
import CompPoly.ToMathlib.Polynomial.BivariateWeightedDegree
import CompPoly.ToMathlib.Polynomial.Div
import CompPoly.Univariate.Barycentric
import CompPoly.Univariate.Basic
import CompPoly.Univariate.BatchEval
import CompPoly.Univariate.BatchEval.Context
import CompPoly.Univariate.BatchEval.Correctness
import CompPoly.Univariate.BatchEval.Naive
import CompPoly.Univariate.BatchEval.SubproductTree
import CompPoly.Univariate.CMvEquiv
import CompPoly.Univariate.CoefficientInterpolation
import CompPoly.Univariate.Context
import CompPoly.Univariate.Deriv
import CompPoly.Univariate.DivisionCorrectness
import CompPoly.Univariate.EuclideanAlgorithm
import CompPoly.Univariate.Lagrange
import CompPoly.Univariate.LagrangeArray
import CompPoly.Univariate.Linear
import CompPoly.Univariate.ManyEval
import CompPoly.Univariate.ManyEval.Basic
import CompPoly.Univariate.ManyEval.Correctness
import CompPoly.Univariate.Modular
import CompPoly.Univariate.NTT.BabyBear
import CompPoly.Univariate.NTT.Domain
import CompPoly.Univariate.NTT.Evaluation
import CompPoly.Univariate.NTT.FastMul
import CompPoly.Univariate.NTT.FastMulLow
import CompPoly.Univariate.NTT.Forward
import CompPoly.Univariate.NTT.Interpolation
import CompPoly.Univariate.NTT.Inverse
import CompPoly.Univariate.NTT.Kernel
import CompPoly.Univariate.NTT.KoalaBear
import CompPoly.Univariate.NTT.Transform
import CompPoly.Univariate.NTTFast.Correctness
import CompPoly.Univariate.NTTFast.Correctness.Basic
import CompPoly.Univariate.NTTFast.Correctness.DIF
import CompPoly.Univariate.NTTFast.Correctness.Pair
import CompPoly.Univariate.NTTFast.Correctness.Pipeline
import CompPoly.Univariate.NTTFast.Correctness.Radix4DIF
import CompPoly.Univariate.NTTFast.Correctness.Radix4DIT
import CompPoly.Univariate.NTTFast.Evaluation
import CompPoly.Univariate.NTTFast.FastMul
import CompPoly.Univariate.NTTFast.FastMulLow
import CompPoly.Univariate.NTTFast.Interpolation
import CompPoly.Univariate.NTTFast.Plan
import CompPoly.Univariate.Quotient.Core
import CompPoly.Univariate.Quotient.Equiv
import CompPoly.Univariate.Raw
import CompPoly.Univariate.Raw.Context
import CompPoly.Univariate.Raw.Core
import CompPoly.Univariate.Raw.Division
import CompPoly.Univariate.Raw.Modular
import CompPoly.Univariate.Raw.Ops
import CompPoly.Univariate.Raw.Proofs
import CompPoly.Univariate.Roots
import CompPoly.Univariate.Roots.Backend
import CompPoly.Univariate.Roots.Context
import CompPoly.Univariate.Roots.Correctness
import CompPoly.Univariate.Roots.Enumeration
import CompPoly.Univariate.Roots.Extraction
import CompPoly.Univariate.Roots.RootProduct
import CompPoly.Univariate.Roots.SmoothSubgroup
import CompPoly.Univariate.Roots.SmoothSubgroup.Basic
import CompPoly.Univariate.Roots.SmoothSubgroup.Correctness
import CompPoly.Univariate.Roots.Splitter
import CompPoly.Univariate.ToPoly
import CompPoly.Univariate.ToPoly.Core
import CompPoly.Univariate.ToPoly.Degree
import CompPoly.Univariate.ToPoly.Equiv
import CompPoly.Univariate.ToPoly.Impl
import CompPoly.Univariate.Vanishing