Main.lean`

GitHub source file

0 declarations, 0 contain sorry, 0 declared as axioms

This file declares nothing itself. It gathers the import below, so a file that imports it gets all of them.

Imports

OAI.Geometry.NilpotentCharts.FilteredBasis

Imported by 259 files

OAI.lean
OAI/Combinatorics/SumProduct/Alignment/AbelianMalcev01.lean
OAI/Combinatorics/SumProduct/Alignment/AbelianMalcev02.lean
OAI/Combinatorics/SumProduct/Alignment/Admissible01.lean
OAI/Combinatorics/SumProduct/Alignment/AffineCoefficient01.lean
OAI/Combinatorics/SumProduct/Alignment/AffineOrbit01.lean
OAI/Combinatorics/SumProduct/Alignment/AlignmentMass01.lean
OAI/Combinatorics/SumProduct/Alignment/AllLevel01.lean
OAI/Combinatorics/SumProduct/Alignment/AllLevel02.lean
OAI/Combinatorics/SumProduct/Alignment/AllLevel03.lean
OAI/Combinatorics/SumProduct/Alignment/AllLevel04.lean
OAI/Combinatorics/SumProduct/Alignment/AllLevel05.lean
OAI/Combinatorics/SumProduct/Alignment/AllLevel06.lean
OAI/Combinatorics/SumProduct/Alignment/AllLevel07.lean
OAI/Combinatorics/SumProduct/Alignment/AllLevel08.lean
OAI/Combinatorics/SumProduct/Alignment/AllLevel09.lean
OAI/Combinatorics/SumProduct/Alignment/AllLevel10.lean
OAI/Combinatorics/SumProduct/Alignment/AllLevel11.lean
OAI/Combinatorics/SumProduct/Alignment/AllLevel12.lean
OAI/Combinatorics/SumProduct/Alignment/AllLevel13.lean
OAI/Combinatorics/SumProduct/Alignment/AllLevel14.lean
OAI/Combinatorics/SumProduct/Alignment/AllLevel15.lean
OAI/Combinatorics/SumProduct/Alignment/BinomialDifference01.lean
OAI/Combinatorics/SumProduct/Alignment/Blocks01.lean
OAI/Combinatorics/SumProduct/Alignment/Blocks02.lean
OAI/Combinatorics/SumProduct/Alignment/BooleanBinomial01.lean
OAI/Combinatorics/SumProduct/Alignment/BooleanRough01.lean
OAI/Combinatorics/SumProduct/Alignment/BooleanRough02.lean
OAI/Combinatorics/SumProduct/Alignment/BoxPolynomial01.lean
OAI/Combinatorics/SumProduct/Alignment/BracketDrift01.lean
OAI/Combinatorics/SumProduct/Alignment/BracketHyperplanes01.lean
OAI/Combinatorics/SumProduct/Alignment/BracketHyperplanes02.lean
OAI/Combinatorics/SumProduct/Alignment/CentralFiber01.lean
OAI/Combinatorics/SumProduct/Alignment/CentralQuotient01.lean
OAI/Combinatorics/SumProduct/Alignment/CharacterFactorization01.lean
OAI/Combinatorics/SumProduct/Alignment/CoefficientPeeling01.lean
OAI/Combinatorics/SumProduct/Alignment/CompactConvex01.lean
OAI/Combinatorics/SumProduct/Alignment/CompactFamily01.lean
OAI/Combinatorics/SumProduct/Alignment/ComparableBox01.lean
OAI/Combinatorics/SumProduct/Alignment/ComparableBox02.lean
OAI/Combinatorics/SumProduct/Alignment/ComparableBox03.lean
OAI/Combinatorics/SumProduct/Alignment/ConstantCoefficient01.lean
OAI/Combinatorics/SumProduct/Alignment/CoordinateSubspace01.lean
OAI/Combinatorics/SumProduct/Alignment/CorrectedBox01.lean
OAI/Combinatorics/SumProduct/Alignment/CorrectedBox02.lean
OAI/Combinatorics/SumProduct/Alignment/CorrectedBox03.lean
OAI/Combinatorics/SumProduct/Alignment/CorrectedBox04.lean
OAI/Combinatorics/SumProduct/Alignment/CorrectedBox05.lean
OAI/Combinatorics/SumProduct/Alignment/CorrectedBox06.lean
OAI/Combinatorics/SumProduct/Alignment/CorrectedBox07.lean
OAI/Combinatorics/SumProduct/Alignment/CoveringSubspace01.lean
OAI/Combinatorics/SumProduct/Alignment/CubeFaces01.lean
OAI/Combinatorics/SumProduct/Alignment/CubeFaces02.lean
OAI/Combinatorics/SumProduct/Alignment/CubeKernel01.lean
OAI/Combinatorics/SumProduct/Alignment/CubeLocal01.lean
OAI/Combinatorics/SumProduct/Alignment/CubeLocal02.lean
OAI/Combinatorics/SumProduct/Alignment/CubeLocal03.lean
OAI/Combinatorics/SumProduct/Alignment/CubeLocal04.lean
OAI/Combinatorics/SumProduct/Alignment/CubeLocal05.lean
OAI/Combinatorics/SumProduct/Alignment/CubeLocal06.lean
OAI/Combinatorics/SumProduct/Alignment/CubeLocal07.lean
OAI/Combinatorics/SumProduct/Alignment/CubeLocal08.lean
OAI/Combinatorics/SumProduct/Alignment/CubeLocal09.lean
OAI/Combinatorics/SumProduct/Alignment/CubeParameter01.lean
OAI/Combinatorics/SumProduct/Alignment/CubePolynomials01.lean
OAI/Combinatorics/SumProduct/Alignment/CubeRational01.lean
OAI/Combinatorics/SumProduct/Alignment/CubeRationalization01.lean
OAI/Combinatorics/SumProduct/Alignment/CubeTaylor01.lean
OAI/Combinatorics/SumProduct/Alignment/CubeTaylor02.lean
OAI/Combinatorics/SumProduct/Alignment/DenseBoolean01.lean
OAI/Combinatorics/SumProduct/Alignment/DenseBox01.lean
OAI/Combinatorics/SumProduct/Alignment/DensePolynomial01.lean
OAI/Combinatorics/SumProduct/Alignment/DenseRough01.lean
OAI/Combinatorics/SumProduct/Alignment/DyadicHarmonic01.lean
OAI/Combinatorics/SumProduct/Alignment/EmbeddedCube01.lean
OAI/Combinatorics/SumProduct/Alignment/FactorCoefficient01.lean
OAI/Combinatorics/SumProduct/Alignment/FejerDetection01.lean
OAI/Combinatorics/SumProduct/Alignment/FilteredShears01.lean
OAI/Combinatorics/SumProduct/Alignment/FiniteCover01.lean
OAI/Combinatorics/SumProduct/Alignment/FiniteMenu01.lean
OAI/Combinatorics/SumProduct/Alignment/FinitePiece01.lean
OAI/Combinatorics/SumProduct/Alignment/FourierObstruction01.lean
OAI/Combinatorics/SumProduct/Alignment/GlobalPoint01.lean
OAI/Combinatorics/SumProduct/Alignment/HarmonicExposure01.lean
OAI/Combinatorics/SumProduct/Alignment/HarmonicExposure02.lean
OAI/Combinatorics/SumProduct/Alignment/HarmonicTranslation01.lean
OAI/Combinatorics/SumProduct/Alignment/HierarchyRates01.lean
OAI/Combinatorics/SumProduct/Alignment/IntegerAlignment01.lean
OAI/Combinatorics/SumProduct/Alignment/IntegerArrays01.lean
OAI/Combinatorics/SumProduct/Alignment/IntegerArrays02.lean
OAI/Combinatorics/SumProduct/Alignment/IntegerArrays03.lean
OAI/Combinatorics/SumProduct/Alignment/IntegerArrays04.lean
OAI/Combinatorics/SumProduct/Alignment/IntegerArrays05.lean
OAI/Combinatorics/SumProduct/Alignment/IntegerArrays06.lean
OAI/Combinatorics/SumProduct/Alignment/IntegerArrays07.lean
OAI/Combinatorics/SumProduct/Alignment/IntegerArrays08.lean
OAI/Combinatorics/SumProduct/Alignment/IntegerArrays09.lean
OAI/Combinatorics/SumProduct/Alignment/IntegerArrays10.lean
OAI/Combinatorics/SumProduct/Alignment/IntegerArrays11.lean
OAI/Combinatorics/SumProduct/Alignment/IntegerArrays12.lean
OAI/Combinatorics/SumProduct/Alignment/IntegerArrays13.lean
OAI/Combinatorics/SumProduct/Alignment/IntegerArrays14.lean
OAI/Combinatorics/SumProduct/Alignment/IntegerArrays15.lean
OAI/Combinatorics/SumProduct/Alignment/IntegerHyperplane01.lean
OAI/Combinatorics/SumProduct/Alignment/IntegerHyperplane02.lean
OAI/Combinatorics/SumProduct/Alignment/LagrangeBounds01.lean
OAI/Combinatorics/SumProduct/Alignment/LeibmanSquare01.lean
OAI/Combinatorics/SumProduct/Alignment/LeibmanSquare02.lean
OAI/Combinatorics/SumProduct/Alignment/LeibmanSquare03.lean
OAI/Combinatorics/SumProduct/Alignment/LeibmanSquare04.lean
OAI/Combinatorics/SumProduct/Alignment/LeibmanSquare05.lean
OAI/Combinatorics/SumProduct/Alignment/MacroSelection01.lean
OAI/Combinatorics/SumProduct/Alignment/MacroSelection02.lean
OAI/Combinatorics/SumProduct/Alignment/MalcevCentral01.lean
OAI/Combinatorics/SumProduct/Alignment/MalcevCharacters01.lean
OAI/Combinatorics/SumProduct/Alignment/MalcevHorizontal01.lean
OAI/Combinatorics/SumProduct/Alignment/MalcevHorizontal02.lean
OAI/Combinatorics/SumProduct/Alignment/MalcevHorizontal03.lean
OAI/Combinatorics/SumProduct/Alignment/MalcevTail01.lean
OAI/Combinatorics/SumProduct/Alignment/MalcevTail02.lean
OAI/Combinatorics/SumProduct/Alignment/MalcevTail03.lean
OAI/Combinatorics/SumProduct/Alignment/MalcevWeighted01.lean
OAI/Combinatorics/SumProduct/Alignment/MalcevWeighted02.lean
OAI/Combinatorics/SumProduct/Alignment/MenuLiteral01.lean
OAI/Combinatorics/SumProduct/Alignment/MicrocellFibers01.lean
OAI/Combinatorics/SumProduct/Alignment/MicrocellHarmonic01.lean
OAI/Combinatorics/SumProduct/Alignment/MicrocellSaturation01.lean
OAI/Combinatorics/SumProduct/Alignment/MicrocellScale01.lean
OAI/Combinatorics/SumProduct/Alignment/NearLattice01.lean
OAI/Combinatorics/SumProduct/Alignment/PairTail01.lean
OAI/Combinatorics/SumProduct/Alignment/PairTail02.lean
OAI/Combinatorics/SumProduct/Alignment/PairTail03.lean
OAI/Combinatorics/SumProduct/Alignment/PairTail04.lean
OAI/Combinatorics/SumProduct/Alignment/PairTail05.lean
OAI/Combinatorics/SumProduct/Alignment/PairTail06.lean
OAI/Combinatorics/SumProduct/Alignment/ParametricSmooth01.lean
OAI/Combinatorics/SumProduct/Alignment/PhysicalDecay01.lean
OAI/Combinatorics/SumProduct/Alignment/PivotExtension01.lean
OAI/Combinatorics/SumProduct/Alignment/PivotExtension02.lean
OAI/Combinatorics/SumProduct/Alignment/PivotPaths01.lean
OAI/Combinatorics/SumProduct/Alignment/PivotPaths02.lean
OAI/Combinatorics/SumProduct/Alignment/PivotPaths03.lean
OAI/Combinatorics/SumProduct/Alignment/PointLaw01.lean
OAI/Combinatorics/SumProduct/Alignment/PointLaw02.lean
OAI/Combinatorics/SumProduct/Alignment/PolynomialArray01.lean
OAI/Combinatorics/SumProduct/Alignment/PolynomialCharacter01.lean
OAI/Combinatorics/SumProduct/Alignment/PolynomialDephasing01.lean
OAI/Combinatorics/SumProduct/Alignment/PolynomialLine01.lean
OAI/Combinatorics/SumProduct/Alignment/PolynomialWeyl01.lean
OAI/Combinatorics/SumProduct/Alignment/ProductExposure01.lean
OAI/Combinatorics/SumProduct/Alignment/ProductExposure02.lean
OAI/Combinatorics/SumProduct/Alignment/ProductExposure03.lean
OAI/Combinatorics/SumProduct/Alignment/ProductExposure04.lean
OAI/Combinatorics/SumProduct/Alignment/ProgressionPartition01.lean
OAI/Combinatorics/SumProduct/Alignment/RationalEchelon01.lean
OAI/Combinatorics/SumProduct/Alignment/RationalEchelon02.lean
OAI/Combinatorics/SumProduct/Alignment/RationalFactor01.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice01.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice02.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice03.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice04.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice05.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice06.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice07.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice08.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice09.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice10.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice11.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice12.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice13.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice14.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice15.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice16.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice17.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice18.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice19.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice20.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice21.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice22.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice23.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice24.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice25.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice26.lean
OAI/Combinatorics/SumProduct/Alignment/RationalLattice27.lean
OAI/Combinatorics/SumProduct/Alignment/RationalQuotient01.lean
OAI/Combinatorics/SumProduct/Alignment/RationalTail01.lean
OAI/Combinatorics/SumProduct/Alignment/RationalTail02.lean
OAI/Combinatorics/SumProduct/Alignment/RationalTriangular01.lean
OAI/Combinatorics/SumProduct/Alignment/RawHarmonic01.lean
OAI/Combinatorics/SumProduct/Alignment/RawMenu.lean
OAI/Combinatorics/SumProduct/Alignment/RegularResidue01.lean
OAI/Combinatorics/SumProduct/Alignment/ResidueAlignment01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughArray01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughArray02.lean
OAI/Combinatorics/SumProduct/Alignment/RoughArray03.lean
OAI/Combinatorics/SumProduct/Alignment/RoughArray04.lean
OAI/Combinatorics/SumProduct/Alignment/RoughCovered01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughCovered02.lean
OAI/Combinatorics/SumProduct/Alignment/RoughCube01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughCube02.lean
OAI/Combinatorics/SumProduct/Alignment/RoughDimension01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughDyadic01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughExtremal01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughFace01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughFace02.lean
OAI/Combinatorics/SumProduct/Alignment/RoughFace03.lean
OAI/Combinatorics/SumProduct/Alignment/RoughInterpolation01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughJoint01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughKernel01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughKernel02.lean
OAI/Combinatorics/SumProduct/Alignment/RoughKernel03.lean
OAI/Combinatorics/SumProduct/Alignment/RoughKernel04.lean
OAI/Combinatorics/SumProduct/Alignment/RoughKernel05.lean
OAI/Combinatorics/SumProduct/Alignment/RoughLiteral01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughLog01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughPhysical01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughProduct01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughProduct02.lean
OAI/Combinatorics/SumProduct/Alignment/RoughProduct03.lean
OAI/Combinatorics/SumProduct/Alignment/RoughRational01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughReal01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughSampling01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughSampling02.lean
OAI/Combinatorics/SumProduct/Alignment/RoughSplit01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughTopological01.lean
OAI/Combinatorics/SumProduct/Alignment/RoughTopological02.lean
OAI/Combinatorics/SumProduct/Alignment/RoughTopological03.lean
OAI/Combinatorics/SumProduct/Alignment/ScalarDifference01.lean
OAI/Combinatorics/SumProduct/Alignment/SmoothBinomial01.lean
OAI/Combinatorics/SumProduct/Alignment/SquareHorizontal01.lean
OAI/Combinatorics/SumProduct/Alignment/SquareInduction01.lean
OAI/Combinatorics/SumProduct/Alignment/SquareInduction02.lean
OAI/Combinatorics/SumProduct/Alignment/SquareInduction03.lean
OAI/Combinatorics/SumProduct/Alignment/SquareInduction04.lean
OAI/Combinatorics/SumProduct/Alignment/SquareInduction05.lean
OAI/Combinatorics/SumProduct/Alignment/SquareInduction06.lean
OAI/Combinatorics/SumProduct/Alignment/SquareInduction07.lean
OAI/Combinatorics/SumProduct/Alignment/SquareInduction08.lean
OAI/Combinatorics/SumProduct/Alignment/SquareInduction09.lean
OAI/Combinatorics/SumProduct/Alignment/SquareInduction10.lean
OAI/Combinatorics/SumProduct/Alignment/SquareInduction11.lean
OAI/Combinatorics/SumProduct/Alignment/SquareInduction12.lean
OAI/Combinatorics/SumProduct/Alignment/SquareInduction13.lean
OAI/Combinatorics/SumProduct/Alignment/SquareInduction14.lean
OAI/Combinatorics/SumProduct/Alignment/TailCharacter01.lean
OAI/Combinatorics/SumProduct/Alignment/TorusVertical01.lean
OAI/Combinatorics/SumProduct/Alignment/TriangularDenominators01.lean
OAI/Combinatorics/SumProduct/Alignment/TriangularLattice01.lean
OAI/Combinatorics/SumProduct/Alignment/UniformSlow01.lean
OAI/Combinatorics/SumProduct/Alignment/UnitInterval01.lean
OAI/Combinatorics/SumProduct/Alignment/WeightedBoxes01.lean
OAI/Combinatorics/SumProduct/Alignment/WeightedLinear01.lean
OAI/Combinatorics/SumProduct/Alignment/WeightedPolynomial01.lean
OAI/Combinatorics/SumProduct/Alignment/WeightedPolynomial02.lean
OAI/Combinatorics/SumProduct/Alignment/WeylInverse01.lean
OAI/Combinatorics/SumProduct/Alignment/WordPlan01.lean
OAI/Combinatorics/SumProduct/Alignment/WordPlan02.lean
OAI/Combinatorics/SumProduct/Alignment/WordPlan03.lean
OAI/Combinatorics/SumProduct/Alignment/WordPlan04.lean