OAI/Geometry/Relativity/CKS/SphericalTensorChart.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSSphericalChart.tensorA line 12
2. def OAI.CKSSphericalChart.tensorB line 13
3. def OAI.CKSSphericalChart.tensorC line 14
4. def OAI.CKSSphericalChart.tensorPhi line 15
5. lemma OAI.CKSSphericalChart.tensorA_smooth line 17
6. lemma OAI.CKSSphericalChart.tensorB_smooth line 19
7. lemma OAI.CKSSphericalChart.tensorC_smooth line 21
8. lemma OAI.CKSSphericalChart.tensorPhi_smooth line 23
9. lemma OAI.CKSSphericalChart.frame_derivatives line 26
10. lemma OAI.CKSSphericalChart.tensor_trace_free line 75