OAI/Analysis/Pureness/GroupAlgebra/FreeGroupMatrixDimensions.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.indexedPermutationUnitary line 11
  2. def OAI.CuntzPureness.freeGroupModelDimension line 29
  3. def OAI.CuntzPureness.freeGroupModelMultiplicity line 33
  4. lemma OAI.CuntzPureness.freeGroupModelDimension_eq line 37
  5. lemma OAI.CuntzPureness.freeGroupModelDimension_pos line 41
  6. lemma OAI.CuntzPureness.freeGroupModelDimension_strictMono line 46
  7. def OAI.CuntzPureness.freeGroupModelCoordinate line 54
  8. lemma OAI.CuntzPureness.freeGroupModelCoordinate_succ line 56
  9. lemma OAI.CuntzPureness.freeGroupModelCoordinate_strictMono line 60
  10. def OAI.CuntzPureness.freeGroupModelIndexEquiv line 67
  11. def OAI.CuntzPureness.freeGroupReplicatedPermutation line 74
  12. lemma OAI.CuntzPureness.freeGroupReplicatedPermutation_no_fixed line 81
  13. def OAI.CuntzPureness.freeGroupReplicatedMatrix line 92
  14. lemma OAI.CuntzPureness.freeGroupReplicatedMatrix_trace line 96