OAI/Geometry/Relativity/CKS/MixedJetCalculus.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CKSMixedGeometry.Mat line 13
  2. abbrev OAI.CKSMixedGeometry.ScalarJet line 14
  3. def OAI.CKSMixedGeometry.actualScalarJet line 15
  4. def OAI.CKSMixedGeometry.constantJet line 18
  5. def OAI.CKSMixedGeometry.productJet line 20
  6. def OAI.CKSMixedGeometry.reciprocalJet line 24
  7. lemma OAI.CKSMixedGeometry.actual_reciprocal line 28
  8. lemma OAI.CKSMixedGeometry.actualScalarJet_const line 41
  9. lemma OAI.CKSMixedGeometry.actualScalarJet_add line 48
  10. lemma OAI.CKSMixedGeometry.actualScalarJet_smul line 66
  11. lemma OAI.CKSMixedGeometry.actualScalarJet_sub line 82
  12. lemma OAI.CKSMixedGeometry.actualScalarJet_mul line 90
  13. lemma OAI.CKSMixedGeometry.productJet_smooth line 101
  14. lemma OAI.CKSMixedGeometry.reciprocalJet_smooth line 105
  15. lemma OAI.CKSMixedGeometry.actualScalarJet_congr line 122
  16. lemma OAI.CKSMixedGeometry.actualScalarJet_linear line 135
  17. lemma OAI.CKSMixedGeometry.actualScalarJet_D_linear line 143
  18. lemma OAI.CKSMixedGeometry.actualScalarJet_neg line 157
  19. lemma OAI.CKSMixedGeometry.actualScalarJet_sum line 161