OAI/Analysis/JiangSu/TraceCone/
368 declarations, 0 contain sorry, 0 declared as axioms; 21 files
Files
- AbsoluteComparison.lean 13 declarations
- CompactDensity.lean 12 declarations
- CompactOperators.lean 23 declarations
- Cuntz.lean 18 declarations
- CuntzDenseMaps.lean 18 declarations
- CuntzIdentities.lean 13 declarations
- FamilyQuotient.lean 4 declarations
- MatrixBlockNorm.lean 19 declarations
- MatrixCorners.lean 9 declarations
- MatrixEmbedding.lean 28 declarations
- MatrixEntries.lean 19 declarations
- MatrixFamilies.lean 1 declarations
- MatrixMasks.lean 31 declarations
- MatrixPositive.lean 16 declarations
- MatrixRestriction.lean 11 declarations
- MatrixSums.lean 28 declarations
- ProductCuts.lean 21 declarations
- Pullback.lean 26 declarations
- Rank.lean 25 declarations
- RankCyclic.lean 19 declarations
- Weights.lean 14 declarations