OAI/Geometry/Borsuk/MatrixGeometry/ReflectionTransport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.householder line 10
2. lemma OAI.BorsukNine.householder_apply line 13
3. lemma OAI.BorsukNine.householder_send line 18
4. lemma OAI.BorsukNine.householder_orthogonal line 23
5. lemma OAI.BorsukNine.householder_at_self line 30
6. lemma OAI.BorsukNine.householder_joint_continuousOn line 35
7. lemma OAI.BorsukNine.householder_joint_contDiffOn line 49