OAI/Analysis/KadisonSimilarity/FreeProduct/FreeCreationOperators.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Centered-letter creation maps on the actual leading-word subspaces.

  1. abbrev OAI.KadisonSimilarity.FreeCreationParameter line 18
  2. def OAI.KadisonSimilarity.freeCreationTensor line 20
  3. def OAI.KadisonSimilarity.freeCreationVector line 25
  4. theorem OAI.KadisonSimilarity.freeCreationTensor_total line 28
  5. theorem OAI.KadisonSimilarity.freeCreationGram line 38
  6. def OAI.KadisonSimilarity.freeCreationIsometry line 52
  7. theorem OAI.KadisonSimilarity.freeCreationIsometry_tensor line 58
  8. theorem OAI.KadisonSimilarity.freeCreationIsometry_mem line 67
  9. theorem OAI.KadisonSimilarity.freeCreationIsometry_left line 83