OAI/Geometry/PrescribedRicci/CalabiTensorAlgebra.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Calabi Tensor Algebra.

  1. abbrev OAI.MongeAmpere.TensorIndex line 13
  2. def OAI.MongeAmpere.tensor3 line 15
  3. lemma OAI.MongeAmpere.tensor3_apply line 19
  4. lemma OAI.MongeAmpere.tensor3_mul line 23
  5. lemma OAI.MongeAmpere.tensor3_one line 28
  6. lemma OAI.MongeAmpere.tensor3_mulVec_left line 31
  7. lemma OAI.MongeAmpere.tensor3_mulVec_middle line 37
  8. lemma OAI.MongeAmpere.tensor3_mulVec_right line 43
  9. def OAI.MongeAmpere.tensorMetric line 49
  10. def OAI.MongeAmpere.tensorConnection line 52
  11. lemma OAI.MongeAmpere.tensorMetric_posDef line 55
  12. lemma OAI.MongeAmpere.tensorConnection_mulVec line 58
  13. lemma OAI.MongeAmpere.tensorMetric_mul_connection line 66