OAI/Analysis/JiangSu/TensorProducts/
203 declarations, 0 contain sorry, 0 declared as axioms; 19 files
Files
- CanonicalSpatial.lean 5 declarations
- CommutingStarTensor.lean 17 declarations
- FaithfulTensorCrossNorm.lean 12 declarations
- FaithfulTensorExtension.lean 8 declarations
- FiniteHilbertAmplification.lean 12 declarations
- HilbertTensorCache.lean 5 declarations
- MatrixTensorDecomposition.lean 11 declarations
- NonUnitalCStarCompletion.lean 3 imports, no declarations
- RationalStarHomExtension.lean 9 declarations
- SimpleCStarAlgebraic.lean 6 declarations
- Spatial.lean 14 declarations
- SpatialCompactTensor.lean 8 declarations
- SpatialFiniteMatrices.lean 32 declarations
- SpatialIdentification.lean 21 declarations
- StarHomClosureExtension.lean 8 declarations
- StarTensorMap.lean 7 declarations
- TensorCStarWeights.lean 1 declarations
- TensorIdeal.lean 4 declarations
- TensorSliceSeparation.lean 23 declarations