OAI/Geometry/PrescribedPotential/GlobalOperator.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Global Operator.

  1. lemma OAI.MatrixSmoothGeneral.determinant line 19
  2. lemma OAI.MatrixSmoothGeneral.adjugate line 30
  3. lemma OAI.MatrixSmoothGeneral.inverse line 50
  4. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.transition_det_isUnit line 60
  5. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.linearizedMongeAmpere_compatibility line 69
  6. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.laplacianValue line 90
  7. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.laplacianValue_local line 93
  8. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.linearizedMongeAmpere_smooth line 98
  9. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.laplacian line 115
  10. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.laplacian_localExpression line 123