OAI/Geometry/Relativity/CKS/CKSTensorRealization.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSMixedGeometry.actual_tensorH line 12
2. lemma OAI.CKSMixedGeometry.tensorCrossField_diff line 20
3. lemma OAI.CKSMixedGeometry.tensorQuadField_diff line 27
4. lemma OAI.CKSMixedGeometry.actual_tensorCross line 36
5. lemma OAI.CKSMixedGeometry.actual_tensorQuad line 48
6. lemma OAI.CKSMixedGeometry.tensorLapseSqField_diff line 71
7. lemma OAI.CKSMixedGeometry.tensorLapseField_diff line 78
8. lemma OAI.CKSMixedGeometry.actual_tensorL line 87
9. lemma OAI.CKSMixedGeometry.actual_tensorEta line 106
10. lemma OAI.CKSMixedGeometry.actual_tensorTau line 127
11. lemma OAI.CKSMixedGeometry.tensorLField_diff line 144
12. lemma OAI.CKSMixedGeometry.tensorEtaField_diff line 154
13. lemma OAI.CKSMixedGeometry.tensorTauField_diff line 162