OAI/Geometry/Relativity/CKS/SphericalTensor.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSSphericalChart.pair line 13
  2. def OAI.CKSSphericalChart.dPair line 15
  3. lemma OAI.CKSSphericalChart.pair_symm line 18
  4. lemma OAI.CKSSphericalChart.pair_zero_left line 29
  5. lemma OAI.CKSSphericalChart.pair_zero_right line 30
  6. lemma OAI.CKSSphericalChart.pair_smul_left line 31
  7. lemma OAI.CKSSphericalChart.pair_smul_right line 33
  8. lemma OAI.CKSSphericalChart.pair_neg_left line 41
  9. lemma OAI.CKSSphericalChart.pair_neg_right line 43
  10. lemma OAI.CKSSphericalChart.pair_add_left line 45
  11. lemma OAI.CKSSphericalChart.pair_add_right line 48
  12. lemma OAI.CKSSphericalChart.dPair_smul_dir line 51
  13. lemma OAI.CKSSphericalChart.pair_normal line 60
  14. lemma OAI.CKSSphericalChart.pair_trace line 71
  15. lemma OAI.CKSSphericalChart.dPair_symm line 82
  16. lemma OAI.CKSSphericalChart.pair_smooth line 91
  17. lemma OAI.CKSSphericalChart.D_sum line 101
  18. lemma OAI.CKSSphericalChart.pair_derivative line 106