OAI/Analysis/Commutator/MatrixModules.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Kadison.MatrixModules.corner line 20
  2. lemma OAI.Kadison.MatrixModules.corner_fixed line 22
  3. def OAI.Kadison.MatrixModules.coordinates line 28
  4. def OAI.Kadison.MatrixModules.recombine line 34
  5. lemma OAI.Kadison.MatrixModules.coordinates_apply line 38
  6. lemma OAI.Kadison.MatrixModules.recombine_apply line 41
  7. lemma OAI.Kadison.MatrixModules.coordinates_recombine line 45
  8. lemma OAI.Kadison.MatrixModules.recombine_coordinates line 61
  9. def OAI.Kadison.MatrixModules.moduleEquiv line 72
  10. lemma OAI.Kadison.MatrixModules.moduleEquiv_intertwines line 78
  11. def OAI.Kadison.MatrixModules.basisCopies line 102
  12. lemma OAI.Kadison.MatrixModules.basisCopies_apply line 107
  13. def OAI.Kadison.MatrixModules.inflate line 110
  14. lemma OAI.Kadison.MatrixModules.inflate_mulVec line 114
  15. lemma OAI.Kadison.MatrixModules.basisCopies_intertwines line 119
  16. def OAI.Kadison.MatrixModules.representationEquiv line 131
  17. lemma OAI.Kadison.MatrixModules.representationEquiv_intertwines line 134