OAI/Analysis/JiangSu/MatrixAlgebras/
219 declarations, 0 contain sorry, 0 declared as axioms; 28 files
Files
- CStarProjectionRounding.lean 5 declarations
- CompletedCornerRange.lean 6 declarations
- ContinuousMatrixTraceIdeal.lean 14 declarations
- CornerCompletion.lean 1 declarations
- CornerCompression.lean 19 declarations
- FamilyProjectionLiftTraces.lean 2 declarations
- FinOneMatrixTransport.lean 7 declarations
- FiniteCorners.lean 2 declarations
- FiniteMatrixLimit.lean 2 declarations
- MatrixDiagonalComposition.lean 12 declarations
- MatrixDiagonalTrace.lean 3 declarations
- MatrixFiberCommutants.lean 6 declarations
- MatrixPackingCornerRound.lean 11 declarations
- MatrixPartialFlips.lean 32 declarations
- MatrixProjectionGenerators.lean 14 declarations
- MatrixProjectionTests.lean 9 declarations
- MatrixSimplicity.lean 5 declarations
- MatrixSmallPacking.lean 19 declarations
- MatrixTraces.lean 10 declarations
- MatrixUnitCorners.lean 6 declarations
- MatrixUnitsHom.lean 20 declarations
- PositiveContinuousRepresentation.lean 1 declarations
- ProjectionDefectRankUpper.lean 1 declarations
- ProjectionGapIsometry.lean 1 declarations
- ProjectionLiftTraces.lean 2 declarations
- SharedMatrixBridge.lean 1 declarations
- TracialMatrixCorners.lean 2 declarations
- TracialMatrixModelExtraction.lean 6 declarations