OAI/Analysis/BoundedHochschild/CentralSupportNormalizedRows.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Complete the row covering a central support by the complementary central projection. The resulting row has square sum one in the given predual.

  1. def OAI.BoundedHochschild.KadisonRingrose.centralSupportRow line 21
  2. lemma OAI.BoundedHochschild.KadisonRingrose.centralSupportRow_square line 26
  3. theorem OAI.BoundedHochschild.KadisonRingrose.centralSupportRow_normalized line 36