OAI/Analysis/Commutator/MatrixScalar.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.MatrixScalar.scalarHom line 23
  2. def OAI.Kadison.MatrixScalar.amplify line 27
  3. lemma OAI.Kadison.MatrixScalar.amplify_apply line 38
  4. def OAI.Kadison.MatrixScalar.scalarMatrix line 41
  5. lemma OAI.Kadison.MatrixScalar.scalarMatrix_apply line 43
  6. lemma OAI.Kadison.MatrixScalar.scalarMatrix_injective line 46
  7. lemma OAI.Kadison.MatrixScalar.map_scalar_left line 52
  8. lemma OAI.Kadison.MatrixScalar.map_scalar_right line 58
  9. lemma OAI.Kadison.MatrixScalar.map_scalar_bimodule line 64
  10. lemma OAI.Kadison.MatrixGNS.flatten_symm_apply line 86
  11. def OAI.Kadison.MatrixGNS.shuffle line 91
  12. lemma OAI.Kadison.MatrixGNS.shuffle_apply line 95