OAI/Analysis/Commutator/EndpointModule2.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.normalizedTrace line 20
2. lemma OAI.Kadison.MatrixModule.inner_vector line 31
3. lemma OAI.Kadison.MatrixModule.norm_vector_single line 40
4. lemma OAI.Kadison.MatrixModule.projection_symmetric line 52
5. lemma OAI.Kadison.MatrixModule.projection_fixes_single line 61
6. lemma OAI.Kadison.MatrixModule.endpoint_unit_bound line 72