OAI/Analysis/Pureness/Tensor/SpatialTraceAgreement.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CuntzPureness.shared_completedCompress line 12
2. lemma OAI.CuntzPureness.shared_matrixTraceLinear line 20
3. theorem OAI.CuntzPureness.shared_matrixExtendedTrace_eq line 23
4. lemma OAI.CuntzPureness.completedSpatial_inverse line 37
5. theorem OAI.CuntzPureness.spatialTrace_completed line 41
6. theorem OAI.CuntzPureness.spatialRank_completed line 52