OAI/Geometry/Relativity/CKS/MatrixScalarJets.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CKSAngularGeometry.MatrixScalarJet line 11
2. def OAI.CKSAngularGeometry.matrixScalarJets line 13
3. def OAI.CKSAngularGeometry.determinantJet line 16
4. def OAI.CKSAngularGeometry.inverseMatrixJet line 19
5. lemma OAI.CKSAngularGeometry.actualScalarJet_neg line 23
6. lemma OAI.CKSAngularGeometry.actualScalarJet_sum line 27
7. lemma OAI.CKSAngularGeometry.actual_determinantJet line 41
8. lemma OAI.CKSAngularGeometry.actual_inverseMatrixJet line 49
9. lemma OAI.CKSAngularGeometry.determinantJet_value line 69
10. lemma OAI.CKSAngularGeometry.determinantJet_smooth line 72
11. lemma OAI.CKSAngularGeometry.inverseMatrixJet_smooth line 77