OAI/Analysis/Pureness/GroupAlgebra/ReducedGroupTrace.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CuntzPureness.(instance at line 12) line 12
2. instance OAI.CuntzPureness.(instance at line 14) line 14
3. instance OAI.CuntzPureness.(instance at line 16) line 16
4. instance OAI.CuntzPureness.reducedGroupStarOrderedRing line 18
5. instance OAI.CuntzPureness.(instance at line 20) line 20
6. def OAI.CuntzPureness.groupVacuumFunctional line 23
7. lemma OAI.CuntzPureness.groupVacuumFunctional_apply line 29
8. lemma OAI.CuntzPureness.groupVacuumFunctional_square line 32
9. lemma OAI.CuntzPureness.groupVacuumFunctional_one line 38
10. lemma OAI.CuntzPureness.groupVacuumFunctional_generator line 42
11. lemma OAI.CuntzPureness.groupVacuumFunctional_generator_cycle line 48
12. theorem OAI.CuntzPureness.groupVacuumFunctional_tracial line 63
13. lemma OAI.CuntzPureness.groupVacuumFunctional_nonneg line 80
14. def OAI.CuntzPureness.reducedGroupTracialState line 92
15. lemma OAI.CuntzPureness.reducedGroupTracialState_apply line 106
16. theorem OAI.CuntzPureness.reducedGroupTracialState_faithful line 109