OAI/Geometry/Relativity/CKS/MixedMassFields.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CKSMixedGeometry.MassFields line 14
  2. structure OAI.CKSMixedGeometry.MassFields.RegularAt line 25
  3. def OAI.CKSMixedGeometry.massInputOf line 36
  4. def OAI.CKSMixedGeometry.cksQField line 42
  5. def OAI.CKSMixedGeometry.cksHField line 45
  6. def OAI.CKSMixedGeometry.cksLieField line 48
  7. def OAI.CKSMixedGeometry.cksDField line 51
  8. def OAI.CKSMixedGeometry.cksTField line 55
  9. def OAI.CKSMixedGeometry.cksBBField line 59
  10. def OAI.CKSMixedGeometry.cksVField line 62
  11. def OAI.CKSMixedGeometry.cksFField line 66
  12. def OAI.CKSMixedGeometry.cksLeadingField line 69
  13. lemma OAI.CKSMixedGeometry.cksQField_diff line 73
  14. lemma OAI.CKSMixedGeometry.cksHField_diff line 77
  15. lemma OAI.CKSMixedGeometry.cksLieField_diff line 87
  16. lemma OAI.CKSMixedGeometry.cksDField_diff line 94
  17. lemma OAI.CKSMixedGeometry.cksTField_diff line 104
  18. lemma OAI.CKSMixedGeometry.cksBBField_diff line 113
  19. lemma OAI.CKSMixedGeometry.cksVField_diff line 122
  20. lemma OAI.CKSMixedGeometry.cksQField_realized line 130
  21. lemma OAI.CKSMixedGeometry.cksHField_realized line 140
  22. lemma OAI.CKSMixedGeometry.cksLieField_realized line 156