OAI/Geometry/Relativity/CKS/CollarMomentumNormalization.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSAngularGeometry.covectorDiv_rescale line 12
  2. lemma OAI.CKSAngularGeometry.tensorDiv_rescale line 17
  3. lemma OAI.CKSAngularGeometry.covectorPair_rescale line 22
  4. lemma OAI.CKSAngularGeometry.tensorPair_rescale line 26
  5. lemma OAI.CKSAngularGeometry.covectorLie_smul line 30
  6. def OAI.CKSAngularGeometry.physicalLJet line 35
  7. def OAI.CKSAngularGeometry.physicalTJet line 36
  8. def OAI.CKSAngularGeometry.coordinateQ line 38
  9. def OAI.CKSAngularGeometry.coordinateZ line 45
  10. theorem OAI.CKSAngularGeometry.coordinateQ_factor line 50
  11. theorem OAI.CKSAngularGeometry.coordinateZ_factor line 62