OAI/Analysis/Commutator/PaulsenSystem.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.Paulsen.system line 23
  2. lemma OAI.Kadison.Paulsen.one_mem line 38
  3. lemma OAI.Kadison.Paulsen.star_mem line 41
  4. def OAI.Kadison.Paulsen.scalarExtract line 49
  5. lemma OAI.Kadison.Paulsen.scalarExtract_scalar line 51
  6. lemma OAI.Kadison.Paulsen.scalar_reconstruct00 line 54
  7. lemma OAI.Kadison.Paulsen.scalar_reconstruct11 line 59
  8. def OAI.Kadison.Paulsen.sharp line 64
  9. def OAI.Kadison.Paulsen.systemMap line 69
  10. lemma OAI.Kadison.Paulsen.systemMap00 line 82
  11. lemma OAI.Kadison.Paulsen.systemMap01 line 85
  12. lemma OAI.Kadison.Paulsen.systemMap10 line 87
  13. lemma OAI.Kadison.Paulsen.systemMap11 line 90
  14. lemma OAI.Kadison.Paulsen.systemMap_one line 93