OAI/Geometry/Relativity/CKS/CollarThinPrimitives.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSAngularGeometry.thinTensor line 12
  2. def OAI.CKSAngularGeometry.thinRaw line 14
  3. lemma OAI.CKSAngularGeometry.thinQ line 17
  4. lemma OAI.CKSAngularGeometry.thinC line 18
  5. lemma OAI.CKSAngularGeometry.thinD line 19
  6. lemma OAI.CKSAngularGeometry.thinT line 20
  7. lemma OAI.CKSAngularGeometry.thinF line 21
  8. lemma OAI.CKSAngularGeometry.thinL line 22
  9. lemma OAI.CKSAngularGeometry.thinTr line 23
  10. lemma OAI.CKSAngularGeometry.thinA line 24
  11. lemma OAI.CKSAngularGeometry.thinX line 28
  12. lemma OAI.CKSAngularGeometry.thin_mz line 35
  13. lemma OAI.CKSAngularGeometry.thin_mw line 37
  14. lemma OAI.CKSAngularGeometry.thin_mq line 39
  15. lemma OAI.CKSAngularGeometry.thin_mS line 42
  16. lemma OAI.CKSAngularGeometry.thin_mE line 44
  17. lemma OAI.CKSAngularGeometry.thin_mT line 46
  18. lemma OAI.CKSAngularGeometry.thin_mEr line 51
  19. lemma OAI.CKSAngularGeometry.thin_mX line 53
  20. lemma OAI.CKSAngularGeometry.thin_mc0 line 56
  21. lemma OAI.CKSAngularGeometry.thin_mc1 line 59
  22. lemma OAI.CKSAngularGeometry.thin_mc2 line 62
  23. lemma OAI.CKSAngularGeometry.thin_mc4 line 65
  24. lemma OAI.CKSAngularGeometry.thin_mc3 line 68
  25. lemma OAI.CKSAngularGeometry.thin_nF line 71
  26. lemma OAI.CKSAngularGeometry.thin_nFr line 74