OAI/Geometry/Relativity/CKS/SchwarzschildCartesianDerivatives.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSSchwarzschild.norm_derivative line 12
2. lemma OAI.CKSSchwarzschild.radialUnit_derivative line 25
3. lemma OAI.CKSSchwarzschild.radial_inner_derivative line 37
4. lemma OAI.CKSSchwarzschild.radial_metric_derivative line 46
5. lemma OAI.CKSSchwarzschild.radialNormal_derivative line 61