OAI/Geometry/IsometricImmersion/Curvature/AffineConnection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Geometry.AffineCalculus.coordPartial_const_mul_at line 14
  2. theorem OAI.SmoothLocal.Geometry.AffineCalculus.coordPartial_mul_const_at line 19
  3. theorem OAI.SmoothLocal.Geometry.coordPartial_affine_comp line 26
  4. theorem OAI.SmoothLocal.Geometry.coordPartial_affinePullbackMetric line 36
  5. theorem OAI.SmoothLocal.Geometry.christoffelFirstKind_affinePullback line 67
  6. theorem OAI.SmoothLocal.Geometry.christoffel_affinePullback_push line 78