OAI/Analysis/Commutator/MatrixFlatten.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.MatrixGNS.flattenHom line 26
2. lemma OAI.Kadison.MatrixGNS.flattenHom_bijective line 63
3. def OAI.Kadison.MatrixGNS.flatten line 72
4. lemma OAI.Kadison.MatrixGNS.flatten_apply line 76
5. lemma OAI.Kadison.MatrixGNS.trace_flatten line 79
6. def OAI.Kadison.MatrixGNS.flatBalancedUnitary line 86
7. lemma OAI.Kadison.MatrixGNS.flatBalancedUnitary_sq line 96
8. lemma OAI.Kadison.MatrixGNS.flatBalancedUnitary_trace line 103