OAI/Analysis/Pureness/GroupAlgebra/GroupRegularRepresentation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.groupL2Perm line 10
  2. abbrev OAI.CuntzPureness.GroupL2 line 25
  3. abbrev OAI.CuntzPureness.GroupOperator line 26
  4. def OAI.CuntzPureness.groupLeft line 28
  5. def OAI.CuntzPureness.groupRight line 30
  6. lemma OAI.CuntzPureness.groupLeft_apply line 32
  7. lemma OAI.CuntzPureness.groupRight_apply line 33
  8. lemma OAI.CuntzPureness.groupLeft_one line 35
  9. lemma OAI.CuntzPureness.groupLeft_mul line 36
  10. lemma OAI.CuntzPureness.groupRight_one line 38
  11. lemma OAI.CuntzPureness.groupRight_mul line 39
  12. lemma OAI.CuntzPureness.groupLeft_star line 42
  13. lemma OAI.CuntzPureness.groupRight_star line 49
  14. lemma OAI.CuntzPureness.groupLeft_commute_right line 56
  15. def OAI.CuntzPureness.groupLeftUnitary line 59
  16. def OAI.CuntzPureness.groupVacuum line 65
  17. lemma OAI.CuntzPureness.groupVacuum_norm line 67
  18. lemma OAI.CuntzPureness.groupLeft_vacuum line 71
  19. lemma OAI.CuntzPureness.groupRight_vacuum line 76
  20. lemma OAI.CuntzPureness.groupVacuum_inner line 81