OAI/Geometry/Borsuk/MatrixGeometry/MatrixReflection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.rankOne_continuous line 16
2. def OAI.BorsukNine.reflectionMatrix line 22
3. lemma OAI.BorsukNine.reflectionMatrix_action line 25
4. lemma OAI.BorsukNine.reflectionMatrix_eq line 33
5. lemma OAI.BorsukNine.householder_involutive line 40
6. lemma OAI.BorsukNine.reflectionMatrix_conjugate line 43
7. lemma OAI.BorsukNine.reflectionMatrix_continuousOn line 55
8. lemma OAI.BorsukNine.householder_matrix_joint_continuousOn line 64