OAI/Analysis/Commutator/FactorGeneratedSpace.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.CbFactor.generated line 19
2. instance OAI.Kadison.CbFactor.(instance at line 22) line 22
3. lemma OAI.Kadison.CbFactor.generated_generator line 25
4. lemma OAI.Kadison.CbFactor.generated_right line 29
5. lemma OAI.Kadison.CbFactor.generated_invariant line 32
6. lemma OAI.Kadison.CbFactor.generated_projection_commutes line 44
7. lemma OAI.Kadison.CbFactor.generated_projection_right line 55
8. lemma OAI.Kadison.CbFactor.factor_intertwines_on_generated line 65
9. def OAI.Kadison.CbFactor.leftCompression line 81
10. lemma OAI.Kadison.CbFactor.leftCompression_right line 84
11. lemma OAI.Kadison.CbFactor.leftCompression_intertwines line 89