OAI/Geometry/Relativity/CKS/CKSMassFields.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CKSAngularGeometry.MassFields line 12
  2. structure OAI.CKSAngularGeometry.MassFields.RegularAt line 23
  3. def OAI.CKSAngularGeometry.massInputOf line 34
  4. def OAI.CKSAngularGeometry.cksQField line 40
  5. def OAI.CKSAngularGeometry.cksHField line 43
  6. def OAI.CKSAngularGeometry.cksLieField line 46
  7. def OAI.CKSAngularGeometry.cksDField line 49
  8. def OAI.CKSAngularGeometry.cksTField line 53
  9. def OAI.CKSAngularGeometry.cksBBField line 57
  10. def OAI.CKSAngularGeometry.cksVField line 60
  11. def OAI.CKSAngularGeometry.cksFField line 64
  12. def OAI.CKSAngularGeometry.cksLeadingField line 67
  13. lemma OAI.CKSAngularGeometry.cksQField_diff line 71
  14. lemma OAI.CKSAngularGeometry.cksHField_diff line 74
  15. lemma OAI.CKSAngularGeometry.cksLieField_diff line 83
  16. lemma OAI.CKSAngularGeometry.cksDField_diff line 89
  17. lemma OAI.CKSAngularGeometry.cksTField_diff line 97
  18. lemma OAI.CKSAngularGeometry.cksBBField_diff line 104
  19. lemma OAI.CKSAngularGeometry.cksVField_diff line 112
  20. lemma OAI.CKSAngularGeometry.cksQField_realized line 118
  21. lemma OAI.CKSAngularGeometry.cksHField_realized line 125
  22. lemma OAI.CKSAngularGeometry.cksLieField_realized line 132