OAI/Analysis/Commutator/ReplicaPacking.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.PartialIsometryOrder.PartialDecomposition.finitePacking line 29
2. lemma OAI.Kadison.PartialIsometryOrder.PartialDecomposition.finitePacking_star_mul line 33
3. lemma OAI.Kadison.PartialIsometryOrder.PartialDecomposition.finitePacking_norm_le line 51
4. lemma OAI.Kadison.PartialIsometryOrder.PartialDecomposition.finitePacking_mul_val line 57
5. theorem OAI.Kadison.PartialIsometryOrder.PartialDecomposition.exists_packing line 66
6. lemma OAI.Kadison.PartialIsometryOrder.PartialDecomposition.packing_isometry line 83
7. lemma OAI.Kadison.PartialIsometryOrder.PartialDecomposition.packings_orthogonal line 103