OAI/Geometry/Relativity/CKS/CollarFieldJets.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CKSAngularGeometry.CollarCoefficientFields line 13
  2. def OAI.CKSAngularGeometry.CollarCoefficientFields.RegularAt line 23
  3. def OAI.CKSAngularGeometry.fieldRaw line 29
  4. def OAI.CKSAngularGeometry.fieldQ line 41
  5. def OAI.CKSAngularGeometry.fieldQr line 44
  6. def OAI.CKSAngularGeometry.fieldS line 47
  7. def OAI.CKSAngularGeometry.fieldC line 50
  8. def OAI.CKSAngularGeometry.fieldD line 53
  9. def OAI.CKSAngularGeometry.fieldT line 56
  10. def OAI.CKSAngularGeometry.fieldF line 58
  11. def OAI.CKSAngularGeometry.fieldL line 61
  12. def OAI.CKSAngularGeometry.fieldTr line 63
  13. lemma OAI.CKSAngularGeometry.fieldQ_diff line 66
  14. lemma OAI.CKSAngularGeometry.fieldQr_diff line 68
  15. lemma OAI.CKSAngularGeometry.fieldS_diff line 70
  16. lemma OAI.CKSAngularGeometry.field_rawQ line 73
  17. lemma OAI.CKSAngularGeometry.field_rawQr line 79
  18. lemma OAI.CKSAngularGeometry.field_rawS line 85