OAI/Geometry/PrescribedRicci/ChernPairDifferential.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Chern Pair Differential.

  1. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.holVector line 17
  2. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.barVector line 20
  3. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.holArray line 23
  4. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.barArray line 26
  5. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.hermPair_smooth line 29
  6. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.hermPair_hol line 41
  7. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.hermPair_bar line 63
  8. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.covHol line 85
  9. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.covHol_smooth line 88
  10. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.hermPair_hol_compatible line 96
  11. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.hermPair_bar_compatible line 107