OAI/Analysis/JiangSu/TensorProducts/MatrixTensorDecomposition.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixTensor.single line 15
2. lemma OAI.MatrixTensor.single_tensor line 17
3. lemma OAI.MatrixTensor.matrix_eq_sum_single line 26
4. lemma OAI.MatrixTensor.mem_of_pure_tensors line 31
5. lemma OAI.MatrixTensor.fiberAlgebra_top_top line 41
6. lemma OAI.MatrixTensor.left_mem_fiber line 47
7. lemma OAI.MatrixTensor.right_mem_fiber line 50
8. lemma OAI.MatrixTensor.fiberAlgebra_mono line 54
9. lemma OAI.JiangSuConstruction.permutationUnitary_one line 67
10. lemma OAI.JiangSuConstruction.permutationUnitary_mul line 72
11. lemma OAI.JiangSuConstruction.permutationUnitary_apply line 79