OAI/Analysis/Pureness/Stabilization/CompactMatrixUnits.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzTrace.standardVector line 9
  2. lemma OAI.CuntzTrace.inner_standardVector line 10
  3. lemma OAI.CuntzTrace.norm_standardVector line 12
  4. def OAI.CuntzTrace.compactMatrixUnit line 15
  5. theorem OAI.CuntzTrace.compactMatrixUnit_star line 18
  6. theorem OAI.CuntzTrace.compactMatrixUnit_mul line 22
  7. theorem OAI.CuntzTrace.compactMatrixUnit_norm line 30
  8. def OAI.CuntzTrace.compactProjection line 34
  9. lemma OAI.CuntzTrace.compactProjection_star line 36
  10. lemma OAI.CuntzTrace.compactProjection_mul line 38
  11. theorem OAI.CuntzTrace.compactProjection_compress line 42