OAI/Analysis/Pureness/Operators/UnitaryGroupGeneratedAlgebra.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.unitaryGroupSpan line 11
2. def OAI.CuntzPureness.unitaryGroupAlgebra line 47
3. instance OAI.CuntzPureness.unitaryGroupAlgebra_closed line 49
4. instance OAI.CuntzPureness.unitaryGroupAlgebra_cstar line 51
5. instance OAI.CuntzPureness.(instance at line 53) line 53
6. instance OAI.CuntzPureness.(instance at line 55) line 55
7. instance OAI.CuntzPureness.(instance at line 57) line 57
8. instance OAI.CuntzPureness.unitaryGroupAlgebra_starOrdered line 59
9. instance OAI.CuntzPureness.(instance at line 61) line 61
10. lemma OAI.CuntzPureness.unitaryGroup_mem line 64
11. def OAI.CuntzPureness.unitaryGroupGenerator line 67
12. lemma OAI.CuntzPureness.unitaryGroupGenerator_dense line 75
13. def OAI.CuntzPureness.unitaryGroupTracialState line 107
14. lemma OAI.CuntzPureness.unitaryGroupTracialState_apply line 110
15. lemma OAI.CuntzPureness.unitaryGroupTracialState_faithful line 113