OAI/Geometry/Relativity/CKS/CollarFieldTensor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSAngularGeometry.traceFreeField line 11
  2. lemma OAI.CKSAngularGeometry.traceFreeField_diff line 14
  3. lemma OAI.CKSAngularGeometry.actual_traceFreeJet line 22
  4. def OAI.CKSAngularGeometry.fieldEta line 35
  5. def OAI.CKSAngularGeometry.fieldTau line 37
  6. def OAI.CKSAngularGeometry.fieldEr line 40
  7. def OAI.CKSAngularGeometry.fieldX line 43
  8. lemma OAI.CKSAngularGeometry.field_rawEta line 46
  9. lemma OAI.CKSAngularGeometry.field_rawTau line 52
  10. lemma OAI.CKSAngularGeometry.field_rawX line 61