OAI/Analysis/JiangSu/Absorption/CentralHalfFlipIntertwining.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CStarAbsorption.CentralHalfFlipTransfer line 22
2. theorem OAI.CStarAbsorption.quotient_conjugacy_of_transfer line 29
3. theorem OAI.CStarAbsorption.equiv_of_central_half_flip line 70
4. def OAI.CStarAbsorption.ApproximateInnerHalfFlip line 87
5. theorem OAI.CStarAbsorption.diagonalHom_norm line 91
6. theorem OAI.CStarAbsorption.diagonalHom_injective line 98
7. theorem OAI.CStarAbsorption.central_transfer_of_half_flip line 112
8. theorem OAI.CStarAbsorption.equiv_of_nuclear_half_flip line 142
9. lemma OAI.CStarAbsorption.ConnectedApproximateInnerHalfFlip.toApproximate line 155