OAI/Analysis/Pureness/GroupAlgebra/
294 declarations, 0 contain sorry, 0 declared as axioms; 42 files
Files
- CanonicalCauchyFreeGroupExactness.lean 2 declarations
- CanonicalCauchyFreeGroupTensor.lean 9 declarations
- CauchyFourierIdealApproximation.lean 3 declarations
- CauchyFreeGroupExactness.lean 5 declarations
- CauchyFreeGroupFourier.lean 1 declarations
- CauchyFreeGroupTensorQuotient.lean 6 declarations
- CauchyUniformFourierExactness.lean 2 declarations
- FiniteQuotientInclusions.lean 8 declarations
- FiniteQuotientMatrixExtension.lean 7 declarations
- FreeGroupFiniteRadial.lean 5 declarations
- FreeGroupFiniteSeparation.lean 6 declarations
- FreeGroupFiniteWordBalls.lean 3 declarations
- FreeGroupFirstLetter.lean 3 declarations
- FreeGroupInitialSubgroups.lean 3 declarations
- FreeGroupMatrixApproximation.lean 10 declarations
- FreeGroupMatrixDimensions.lean 14 declarations
- FreeGroupPartialTranslations.lean 15 declarations
- FreeGroupPowersPartition.lean 6 declarations
- FreeGroupRadialKernel.lean 6 declarations
- FreeGroupScalarProduct.lean 11 declarations
- FreeGroupTensorTrace.lean 4 declarations
- FreeGroupUniformMultipliers.lean 6 declarations
- FreeGroupWordChoice.lean 2 declarations
- FreeWordTreeDistance.lean 7 declarations
- GeometricShellSummability.lean 1 declarations
- GroupCoordinateProjection.lean 9 declarations
- GroupRegularRepresentation.lean 20 declarations
- GroupTraceGNS.lean 8 declarations
- GroupTraceReconstruction.lean 10 declarations
- PowersAveraging.lean 1 declarations
- PowersProjectionEstimate.lean 1 declarations
- ReducedFreeGroupAWEmbedding.lean 9 declarations
- ReducedFreeGroupUltraEmbedding.lean 11 declarations
- ReducedGroupCStarAlgebra.lean 10 declarations
- ReducedGroupMatrixCoefficients.lean 2 declarations
- ReducedGroupTrace.lean 16 declarations
- ResidualFiniteQuotientSequence.lean 10 declarations
- SubgroupCosetKernel.lean 3 declarations
- WordAncestorFactorization.lean 8 declarations
- WordMeetKernel.lean 8 declarations
- WordRadialFeature.lean 11 declarations
- WordShellFactorization.lean 12 declarations