OAI/Analysis/Pureness/Comparison/TraceAlgebra.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CuntzComparison.AlgebraicTrace line 11
2. instance OAI.CuntzComparison.(instance at line 15) line 15
3. theorem OAI.CuntzComparison.trace_compression line 18
4. def OAI.CuntzComparison.cornerSymmetry line 40
5. theorem OAI.CuntzComparison.cornerSymmetry_selfAdjoint line 42
6. theorem OAI.CuntzComparison.cornerSymmetry_square line 47
7. theorem OAI.CuntzComparison.cornerSymmetry_supported line 55
8. theorem OAI.CuntzComparison.trace_cornerSymmetry line 63
9. theorem OAI.CuntzComparison.normalized_isometry line 69
10. theorem OAI.CuntzComparison.isometry_range_projection line 79