OAI/Geometry/PrescribedRicci/ChernBianchi.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Chern Bianchi.

  1. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.holDerivative_neg line 15
  2. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.chernCurvature_smooth line 27
  3. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.chernConnection_hol_bar line 39
  4. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.chern_bianchi line 49
  5. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.chernCurvature_contraction line 83