OAI/Geometry/Relativity/CKS/MixedMatrixJets.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSMixedGeometry.component_diff line 13
  2. lemma OAI.CKSMixedGeometry.component_three line 16
  3. abbrev OAI.CKSMixedGeometry.MatrixScalarJet line 20
  4. def OAI.CKSMixedGeometry.matrixScalarJets line 22
  5. def OAI.CKSMixedGeometry.determinantJet line 25
  6. def OAI.CKSMixedGeometry.inverseMatrixJet line 28
  7. lemma OAI.CKSMixedGeometry.actual_determinantJet line 32
  8. lemma OAI.CKSMixedGeometry.actual_inverseMatrixJet line 40
  9. lemma OAI.CKSMixedGeometry.determinantJet_value line 60
  10. lemma OAI.CKSMixedGeometry.determinantJet_smooth line 63
  11. lemma OAI.CKSMixedGeometry.inverseMatrixJet_smooth line 68
  12. abbrev OAI.CKSMixedGeometry.MatrixThreeJet line 77
  13. def OAI.CKSMixedGeometry.matrixThreeJets line 79
  14. def OAI.CKSMixedGeometry.determinantThreeJet line 82
  15. def OAI.CKSMixedGeometry.inverseMatrixThreeJet line 85
  16. lemma OAI.CKSMixedGeometry.actualThreeJet_sum line 89
  17. lemma OAI.CKSMixedGeometry.actual_determinantThreeJet line 103
  18. lemma OAI.CKSMixedGeometry.actual_inverseMatrixThreeJet line 111
  19. lemma OAI.CKSMixedGeometry.determinantThreeJet_value line 131
  20. lemma OAI.CKSMixedGeometry.determinantThreeJet_smooth line 134
  21. lemma OAI.CKSMixedGeometry.inverseMatrixThreeJet_smooth line 139