OAI/Analysis/JiangSu/TensorProducts/Spatial.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.NonunitalGamma.Spatial.spatialCompactAlgebra line 57
2. lemma OAI.NonunitalGamma.Spatial.spatialFinite_mem_compactAlgebra line 61
3. lemma OAI.NonunitalGamma.Spatial.spatialEntry_mem_matrixAlgebra line 71
4. def OAI.NonunitalGamma.Spatial.spatialTensorRight line 84
5. lemma OAI.NonunitalGamma.Spatial.spatialTensor_matrixUnitAlgebra line 93
6. theorem OAI.NonunitalGamma.Spatial.spatialTensor_compact_mem line 139
7. theorem OAI.NonunitalGamma.Spatial.spatialCompactAlgebra_eq_matrixAlgebra line 150
8. theorem OAI.NonunitalGamma.Spatial.spatialRepresentation_range_compact line 163
9. instance OAI.NonunitalGamma.Spatial.spatialCompactAlgebra_closed line 166
10. abbrev OAI.NonunitalGamma.Spatial.SpatialStabilization line 169
11. instance OAI.NonunitalGamma.Spatial.(instance at line 171) line 171
12. def OAI.NonunitalGamma.Spatial.spatialRepresentationInto line 174
13. def OAI.NonunitalGamma.Spatial.spatialEquiv line 185
14. theorem OAI.NonunitalGamma.Spatial.spatialEquiv_norm line 195