OAI/Geometry/Relativity/CKS/PhysicalMomentumCovector.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSAngularGeometry.metricPair_smul_left line 12
  2. lemma OAI.CKSAngularGeometry.metricPair_smul_right line 21
  3. lemma OAI.CKSAngularGeometry.coordinateConnectionVector_add_right line 30
  4. lemma OAI.CKSAngularGeometry.coordinateConnectionVector_smul_right line 37
  5. def OAI.CKSAngularGeometry.coordinateTensorCovariantLast line 48
  6. def OAI.CKSAngularGeometry.coordinateMomentumLinear line 64
  7. lemma OAI.CKSAngularGeometry.coordinateMomentum_expansion line 88
  8. def OAI.CKSAngularGeometry.momentumCovector line 100
  9. theorem OAI.CKSAngularGeometry.physical_momentum_frame_norm line 103
  10. theorem OAI.CKSAngularGeometry.physical_momentum_normal_tangential line 112