OAI/Analysis/KadisonKastler/SupportCompressedMatrix.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Full matrix units transported from a supported corner

  1. def OAI.KadisonKastler.supportCompressedMatrixUnits line 17
  2. theorem OAI.KadisonKastler.supportCompressedMatrixUnits_hom line 38
  3. theorem OAI.KadisonKastler.supportCompressedMatrixUnits_concreteHom line 47
  4. theorem OAI.KadisonKastler.supportCompressedMatrixUnits_mono line 55
  5. theorem OAI.KadisonKastler.supportCompressedMatrixUnits_intertwine line 72
  6. theorem OAI.KadisonKastler.supportCompressedMatrixUnits_intertwine_star line 83