OAI/Geometry/PrescribedRicci/MatrixWirtingerSecond.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Matrix Wirtinger Second.

  1. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.barMatrixForm line 15
  2. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.holMatrixForm line 19
  3. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.fderiv_barDerivative line 23
  4. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.fderiv_holDerivative line 32
  5. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.bar_hol_comm line 41
  6. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.secondDerivative_col_symm line 74
  7. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.secondDerivative_row_symm line 88