OAI/Analysis/Pureness/GroupAlgebra/FreeGroupScalarProduct.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.freeGroupCoordinateModel line 12
  2. lemma OAI.CuntzPureness.freeGroupCoordinateModel_selected line 17
  3. abbrev OAI.CuntzPureness.ScalarMatrixProduct line 28
  4. instance OAI.CuntzPureness.scalarMatrixProductStarMul line 30
  5. def OAI.CuntzPureness.freeGroupScalarProductModel line 33
  6. def OAI.CuntzPureness.freeGroupScalarUltrafilter line 53
  7. lemma OAI.CuntzPureness.freeGroupScalarUltrafilter_free line 56
  8. lemma OAI.CuntzPureness.freeGroupScalarProduct_trace_limit line 60
  9. def OAI.CuntzPureness.scalarMatrixProductQuotient line 74
  10. def OAI.CuntzPureness.freeGroupScalarUltraUnitary line 79
  11. lemma OAI.CuntzPureness.freeGroupScalarUltraUnitary_trace line 85