OAI/Geometry/CylinderCovering/Ruled/MotionJacobian.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RuledApproximation.HyperbolicMotionJacobian.plane_det_id_add_smul line 9
2. theorem OAI.RuledApproximation.HyperbolicMotionJacobian.trace_det_of_opposite_eigenvalues line 20
3. theorem OAI.RuledApproximation.HyperbolicMotionJacobian.deformation_det line 35
4. theorem OAI.RuledApproximation.HyperbolicMotionJacobian.deformation_volume line 43
5. theorem OAI.RuledApproximation.HyperbolicMotionJacobian.deformation_det_bounds line 52