OAI/Geometry/CylinderCovering/Ruled/Jacobian.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RuledApproximation.HyperbolicJacobian.matrix_det_one_add_smul line 9
2. lemma OAI.RuledApproximation.HyperbolicJacobian.plane_det_id_add_smul line 15
3. theorem OAI.RuledApproximation.HyperbolicJacobian.hyperbolicAt_iff line 23
4. theorem OAI.RuledApproximation.HyperbolicJacobian.deformation_det line 39
5. theorem OAI.RuledApproximation.HyperbolicJacobian.fderiv_deformation_det line 47
6. theorem OAI.RuledApproximation.HyperbolicJacobian.deformation_det_pos line 56
7. theorem OAI.RuledApproximation.HyperbolicJacobian.deformation_det_lt_one line 70