OAI/Analysis/Pureness/Completion/
268 declarations, 0 contain sorry, 0 declared as axioms; 37 files
Files
- CStarAlgebraNorm.lean 6 declarations
- CStarNormBoundEquality.lean 2 declarations
- CStarNormCompletion.lean 6 declarations
- CStarNormNonUnitalPullback.lean 3 declarations
- ClosedIdeals.lean 4 declarations
- ClosedStarIdealQuotientCStar.lean 11 declarations
- ClosedStarIdealQuotientNorm.lean 27 declarations
- CompletedBlockSeries.lean 14 declarations
- CompletedCompressions.lean 14 declarations
- CompletedCornerRange.lean 12 declarations
- CompletedFiniteEnvelope.lean 1 declarations
- CompletedHereditaryWeight.lean 2 declarations
- CompletedIncrementApproximation.lean 6 declarations
- CompletedMainConstruction.lean 2 declarations
- CompletedOrthogonalRanks.lean 6 declarations
- CompletedOrthogonalSeries.lean 2 declarations
- CompletedRankClosure.lean 5 declarations
- CompletedRankComparison.lean 2 declarations
- CompletedRankExhaustion.lean 7 declarations
- CompletedRootRank.lean 6 declarations
- CompletedSandwichBudget.lean 1 declarations
- CompletedSharedTrace.lean 5 declarations
- CompletedSourceIncrements.lean 13 declarations
- CompletedSourceLowerBound.lean 3 declarations
- CompletedSpatialBridge.lean 7 declarations
- CompletedSpatialTensorMap.lean 10 declarations
- CompletedTraceScaling.lean 3 declarations
- CompletedTraceTracial.lean 8 declarations
- CompletedTraceWeight.lean 16 declarations
- CompletedUniformComparison.lean 7 declarations
- CornerCompletion.lean 7 declarations
- CornerCompression.lean 9 declarations
- DenseStarCompletionMap.lean 4 declarations
- FilteredQuotientLift.lean 3 declarations
- NonUnitalCStarCompletion.lean 14 declarations
- NonUnitalRoots.lean 9 declarations
- SharedMatrixBridge.lean 11 declarations