OAI/Geometry/Relativity/CKS/SourcePhysicalMass.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSMixedGeometry.sourceMetric line 12
  2. lemma OAI.CKSMixedGeometry.sourceMetric_pullback line 15
  3. lemma OAI.CKSMixedGeometry.sourceGamma_regular line 23
  4. def OAI.CKSMixedGeometry.sourceShift line 29
  5. def OAI.CKSMixedGeometry.sourceSchur line 32
  6. def OAI.CKSMixedGeometry.sourceGammaRadial line 35
  7. def OAI.CKSMixedGeometry.sourceExpansion line 37
  8. def OAI.CKSMixedGeometry.sourcePhysicalMass line 41
  9. lemma OAI.CKSMixedGeometry.sourceShift_regular line 45
  10. lemma OAI.CKSMixedGeometry.sourceShift_pullback line 52
  11. lemma OAI.CKSMixedGeometry.sourceSchur_pullback line 60
  12. lemma OAI.CKSMixedGeometry.normalizedLie_pullback line 69
  13. lemma OAI.CKSMixedGeometry.sourceGammaRadial_pullback line 81
  14. lemma OAI.CKSMixedGeometry.sourceExpansion_pullback line 93
  15. lemma OAI.CKSMixedGeometry.sourcePhysicalMass_pullback line 111