OAI/Analysis/JiangSu/TraceCone/MatrixBlockNorm.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TraceCone.matrixBlockHom_stage line 14
  2. lemma OAI.TraceCone.matrixBlockStarHom_continuous line 21
  3. theorem OAI.TraceCone.matrixBlockHom_norm line 29
  4. theorem OAI.TraceCone.matrixBlockHom_isometry line 40
  5. def OAI.TraceCone.matrixSwapPermutation line 43
  6. lemma OAI.TraceCone.matrixSwapPermutation_apply line 46
  7. theorem OAI.TraceCone.matrixInterleave_swap line 51
  8. def OAI.TraceCone.matrixBlockSwapHom line 62
  9. lemma OAI.TraceCone.matrixBlockPositive_stage line 65
  10. theorem OAI.TraceCone.matrixBlockPositive_comm line 70
  11. theorem OAI.TraceCone.CuntzClass.matrixAdd_comm line 89
  12. def OAI.TraceCone.matrixAssocLeftHom line 97
  13. def OAI.TraceCone.matrixAssocRightHom line 101
  14. lemma OAI.TraceCone.matrixPositiveCore_common_three line 106
  15. lemma OAI.TraceCone.matrixTriple_cuntzClass line 121
  16. theorem OAI.TraceCone.matrixBlockPositive_assoc line 157
  17. theorem OAI.TraceCone.CuntzClass.matrixAdd_assoc line 172
  18. instance OAI.TraceCone.CuntzClass.(instance at line 183) line 183
  19. instance OAI.TraceCone.CuntzClass.matrixAddCommMonoid line 184