OAI/Geometry/Borsuk/MatrixGeometry/FibreTransport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.householder_swap line 15
2. lemma OAI.BorsukNine.matrixConjugate_householder_self line 20
3. def OAI.BorsukNine.fibreTransport line 40
4. lemma OAI.BorsukNine.fibreTransport_nonneg line 43
5. lemma OAI.BorsukNine.fibreTransport_trace line 47
6. lemma OAI.BorsukNine.fibreTransport_kernel line 51
7. lemma OAI.BorsukNine.fibreTransport_self line 57
8. lemma OAI.BorsukNine.fibreTransport_center line 60
9. lemma OAI.BorsukNine.fibreTransport_unit_iff line 65
10. lemma OAI.BorsukNine.fibreTransport_continuousOn line 75