OAI/Geometry/PrescribedPotential/MetricInverseTrace.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Metric Inverse Trace.

  1. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.derivativeMatrix_isUnit line 18
  2. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.inverseTrace_compatibility line 28
  3. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.inverseTraceValue line 36
  4. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.inverseTraceValue_local line 40
  5. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.inverseTrace line 45
  6. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.inverseTrace_local line 54
  7. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.inverseTrace_positive line 60