OAI/Algebra/OddKaplansky/
1374 declarations, 0 contain sorry, 0 declared as axioms; 87 files
Files
- AdmissibleCount.lean 5 declarations
- Amalgam.lean 27 declarations
- AmalgamExtras.lean 3 declarations
- AugmentBound.lean 14 declarations
- AugmentInverse.lean 7 declarations
- Augmentation.lean 28 declarations
- AugmentationMatrices.lean 10 declarations
- BooleanPolynomial.lean 13 declarations
- Cellular.lean 15 declarations
- CoefficientOrder.lean 5 declarations
- Compression.lean 22 declarations
- Construction.lean 19 declarations
- CosetCoordinates.lean 13 declarations
- CosetGreedy.lean 7 declarations
- CosetMatrix.lean 25 declarations
- CosetRectangles.lean 1 declarations
- CyclicCoset.lean 6 declarations
- Diagrams.lean 298 declarations
- FiniteChoice.lean 16 declarations
- FiniteInverse.lean 5 declarations
- Fourier.lean 30 declarations
- FreeBlocks.lean 12 declarations
- FreeShiftCount.lean 3 declarations
- GeneralTransfer.lean 1 declarations
- Gluing.lean 9 declarations
- GraphEdges.lean 29 declarations
- GraphNumerics.lean 12 declarations
- GreedyColumns.lean 5 declarations
- GreedyFormula.lean 7 declarations
- GreedyInverse.lean 1 declarations
- GreedyLift.lean 12 declarations
- GreedyRectangle.lean 8 declarations
- GreedyRing.lean 22 declarations
- Heisenberg.lean 34 declarations
- HeisenbergRepresentation.lean 16 declarations
- HeisenbergSector.lean 19 declarations
- HighCount.lean 6 declarations
- IdempotentFree.lean 10 declarations
- IncidenceCycles.lean 6 declarations
- IndexCut.lean 4 declarations
- LocalAlgebra.lean 5 declarations
- LocalGroup.lean 23 declarations
- Main.lean 22 declarations
- MatrixActions.lean 12 declarations
- MatrixUnits.lean 6 declarations
- ModularGeneric.lean 10 declarations
- ModularSource.lean 11 declarations
- NilpotentBasis.lean 17 declarations
- OrbitBlock.lean 21 declarations
- OrbitSelection.lean 7 declarations
- OrderedBlocks.lean 21 declarations
- OrderedCoordinates.lean 16 declarations
- OrderedGroup.lean 2 declarations
- OrderedMatrices.lean 25 declarations
- OrderedModular.lean 11 declarations
- OrderedOrbits.lean 21 declarations
- OrderedRectangles.lean 4 declarations
- OrderedZero.lean 1 declarations
- Parameters.lean 11 declarations
- PolynomialGrid.lean 2 declarations
- PrescribedGreedy.lean 5 declarations
- PrescribedInverse.lean 4 declarations
- PrescribedSector.lean 1 declarations
- QuadraticTower.lean 31 declarations
- ScalarAlgebra.lean 17 declarations
- SectorConstruction.lean 32 declarations
- SectorFourier.lean 13 declarations
- SectorGreedy.lean 6 declarations
- SectorGroup.lean 25 declarations
- SectorOrbit.lean 18 declarations
- SectorRectangles.lean 5 declarations
- SectorStabilizer.lean 13 declarations
- SimplexCount.lean 11 declarations
- SourceFit.lean 12 declarations
- SourceGluing.lean 19 declarations
- SourceSector.lean 2 declarations
- SquareCertificate.lean 12 declarations
- SquareConstruction.lean 25 declarations
- Transfer.lean 20 declarations
- WeightedGram.lean 6 declarations
- WeightedProjection.lean 9 declarations
- WreathActions.lean 6 declarations
- WreathBasis.lean 6 declarations
- WreathFourier.lean 23 declarations
- WreathLinear.lean 6 declarations
- WreathMultiply.lean 7 declarations
- WreathRepresentation.lean 7 declarations