OAI/Geometry/IsometricImmersion/Curvature/GaussFormula.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.Geometry.isometric_tangents_independent line 10
2. theorem OAI.SmoothLocal.Geometry.normalResidual_eq_secondFundamental_smul line 18
3. theorem OAI.SmoothLocal.Geometry.covHessian_height_eq_normal_mul_secondFundamental line 37