OAI/Geometry/Relativity/CKS/MixedThreeJets.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CKSMixedGeometry.ScalarThreeJet line 12
  2. def OAI.CKSMixedGeometry.actualThreeJet line 13
  3. def OAI.CKSMixedGeometry.constantThreeJet line 15
  4. def OAI.CKSMixedGeometry.productThreeJet line 16
  5. def OAI.CKSMixedGeometry.reciprocalThreeJet line 18
  6. lemma OAI.CKSMixedGeometry.actualThreeJet_const line 21
  7. lemma OAI.CKSMixedGeometry.actualThreeJet_zero line 33
  8. lemma OAI.CKSMixedGeometry.actualThreeJet_linear line 36
  9. lemma OAI.CKSMixedGeometry.actualThreeJet_smul line 44
  10. lemma OAI.CKSMixedGeometry.actualThreeJet_add line 48
  11. lemma OAI.CKSMixedGeometry.actualThreeJet_neg line 53
  12. lemma OAI.CKSMixedGeometry.actualThreeJet_sub line 57
  13. theorem OAI.CKSMixedGeometry.actualThreeJet_mul line 62
  14. theorem OAI.CKSMixedGeometry.actualThreeJet_reciprocal line 82
  15. lemma OAI.CKSMixedGeometry.productThreeJet_smooth line 102
  16. lemma OAI.CKSMixedGeometry.reciprocalThreeJet_smooth line 111