OAI/Analysis/JiangSu/MatrixAlgebras/MatrixFiberCommutants.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixTensor.fiber_commute_left line 15
2. lemma OAI.MatrixTensor.fiber_commute_right line 26
3. lemma OAI.MatrixTensor.qFlow_commute_left_left line 38
4. lemma OAI.MatrixTensor.qFlow_commute_right_left line 43
5. lemma OAI.MatrixTensor.pFlow_commute_left_right line 48
6. lemma OAI.MatrixTensor.pFlow_commute_right_right line 53