OAI/Geometry/Relativity/CKS/PhysicalCovariantTensor.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CKSAngularGeometry.metricPair_add_leftline 12 - lemma
OAI.CKSAngularGeometry.metricPair_add_rightline 16 - lemma
OAI.CKSAngularGeometry.D_metricPair_bilinearline 20 - def
OAI.CKSAngularGeometry.coordinateConnectionVectorline 31 - def
OAI.CKSAngularGeometry.coordinateTensorCovariantline 35 - lemma
OAI.CKSAngularGeometry.coordinateTensorCovariant_product_ruleline 41 - theorem
OAI.CKSAngularGeometry.actualFrameTensorCovariant_coordinateline 57