OAI/Geometry/Borsuk/MatrixGeometry/MatrixTransport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.matrixConjugate line 14
2. lemma OAI.BorsukNine.matrixConjugate_action line 17
3. lemma OAI.BorsukNine.matrixConjugate_nonneg line 22
4. lemma OAI.BorsukNine.matrixConjugate_rankOne line 25
5. lemma OAI.BorsukNine.matrix_operator_trace line 35
6. lemma OAI.BorsukNine.matrixConjugate_trace line 39
7. lemma OAI.BorsukNine.matrixConjugate_kernel line 48
8. lemma OAI.BorsukNine.matrixConjugate_range line 52
9. lemma OAI.BorsukNine.matrixConjugate_selfAdjoint line 58
10. lemma OAI.BorsukNine.matrixConjugate_involutive line 62