OAI/Analysis/Commutator/EndpointGNS.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.TracialGNS.fullSpace line 22
2. abbrev OAI.Kadison.TracialGNS.zeroSpace line 24
3. def OAI.Kadison.TracialGNS.wordConjugation line 26
4. def OAI.Kadison.TracialGNS.stageCoefficient line 39
5. lemma OAI.Kadison.TracialGNS.stageCoefficient_invariant line 46
6. lemma OAI.Kadison.TracialGNS.stageCoefficient_compatible line 69
7. theorem OAI.Kadison.TracialGNS.stageCoefficient_expansion line 81