OAI/Analysis/Pureness/GroupAlgebra/FreeGroupMatrixApproximation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CuntzPureness.freeGroupNatCountable line 10
2. instance OAI.CuntzPureness.freeGroupNatResiduallyFinite line 12
3. abbrev OAI.CuntzPureness.ReducedFreeGroup line 15
4. abbrev OAI.CuntzPureness.FreeGroupMatrixIndex line 17
5. def OAI.CuntzPureness.freeGroupMatrixModel line 19
6. lemma OAI.CuntzPureness.freeGroupMatrixModel_norm line 23
7. theorem OAI.CuntzPureness.freeGroupMatrixModel_trace line 27
8. theorem OAI.CuntzPureness.freeGroupMatrixModel_finite_moments line 38
9. theorem OAI.CuntzPureness.freeGroupMatrixModel_polynomial_trace line 45
10. theorem OAI.CuntzPureness.reducedFreeGroup_trace_faithful line 56