OAI/Analysis/Commutator/InvariantSum.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Kadison.TracialGNS.sumLevel line 41
  2. instance OAI.Kadison.TracialGNS.sumLevelNormed line 43
  3. instance OAI.Kadison.TracialGNS.sumLevelInner line 46
  4. instance OAI.Kadison.TracialGNS.sumLevelComplete line 49
  5. def OAI.Kadison.TracialGNS.sumLeft line 52
  6. def OAI.Kadison.TracialGNS.sumConjugation line 55
  7. lemma OAI.Kadison.TracialGNS.actual_block_conjugation line 94
  8. lemma OAI.Kadison.TracialGNS.actual_block_left line 105
  9. lemma OAI.Kadison.TracialGNS.actual_block_classification line 113
  10. theorem OAI.Kadison.TracialGNS.actual_word_structure line 123