OAI/Analysis/BoundedHochschild/PositiveBlocks.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Normalize the two diagonal entries of a positive two-by-two block.

  1. def OAI.BoundedHochschild.KadisonRingrose.positiveBlock line 17
  2. lemma OAI.BoundedHochschild.KadisonRingrose.positiveBlock_one line 20
  3. lemma OAI.BoundedHochschild.KadisonRingrose.positiveBlock_conjugate line 25
  4. lemma OAI.BoundedHochschild.KadisonRingrose.diag_isUnit line 34
  5. theorem OAI.BoundedHochschild.KadisonRingrose.positiveBlock_nonneg_iff line 43