OAI/Analysis/KadisonKastler/MatrixCornerAutomorphism.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Restricting a matrix automorphism to a fixed diagonal corner

  1. theorem OAI.KadisonKastler.matrixSlot_add line 13
  2. theorem OAI.KadisonKastler.matrixSlot_smul line 18
  3. theorem OAI.KadisonKastler.matrixSlot_zero line 23
  4. def OAI.KadisonKastler.matrixCornerValue line 30
  5. theorem OAI.KadisonKastler.matrixCornerValue_reconstruct line 33
  6. def OAI.KadisonKastler.matrixCornerHom line 37
  7. theorem OAI.KadisonKastler.matrixCornerHom_injective line 74
  8. theorem OAI.KadisonKastler.matrixCornerHom_surjective line 82
  9. def OAI.KadisonKastler.matrixCornerAut line 94
  10. theorem OAI.KadisonKastler.matrixCornerAut_apply line 98