OAI/Analysis/KadisonKastler/CentralVectorSupport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The support of a central vector commutes with the matrix stages

  1. theorem OAI.KadisonKastler.centralVector_support_commutes line 16
  2. theorem OAI.KadisonKastler.matrixCentralVector_support_commutes line 26