OAI/Geometry/Relativity/CKS/PhysicalCurvatureOperator.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSAngularGeometry.covariant_second_pair line 12
2. def OAI.CKSAngularGeometry.covariantDirectionLinear line 45
3. lemma OAI.CKSAngularGeometry.metricPair_sum_left line 65
4. lemma OAI.CKSAngularGeometry.covariant_frame_direction line 69
5. theorem OAI.CKSAngularGeometry.actualFrameCurvature_operator line 85
6. lemma OAI.CKSAngularGeometry.metricPair_sub_left line 103
7. def OAI.CKSAngularGeometry.curvatureVector line 107
8. theorem OAI.CKSAngularGeometry.actualScalar_curvature_trace line 113