OAI/Geometry/Relativity/CKS/AngularDifferentiation.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.CKSAngularGeometry.actualJetline 12 - def
OAI.CKSAngularGeometry.actualScalarJetline 16 - lemma
OAI.CKSAngularGeometry.component_diffline 19 - lemma
OAI.CKSAngularGeometry.inverse_component_diffline 23 - lemma
OAI.CKSAngularGeometry.D_determinantline 34 - theorem
OAI.CKSAngularGeometry.derivative_inverseline 43 - def
OAI.CKSAngularGeometry.connectionline 61 - def
OAI.CKSAngularGeometry.curvatureRicciline 63 - def
OAI.CKSAngularGeometry.physicalScalarline 68