OAI/Geometry/PrescribedRicci/ChernConnection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Chern Connection.

  1. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.holDerivative_congr line 17
  2. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.holDerivative_sub line 22
  3. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.hol_hol_comm line 32
  4. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.chernConnection line 57
  5. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.chernCurvature line 60
  6. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.chernConnection_smooth line 63
  7. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.chernConnection_torsion line 71
  8. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.chernConnection_bar line 79
  9. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.chernConnection_hol line 92
  10. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.chernConnection_maurerCartan line 106