OAI/Geometry/PrescribedPotential/ScalarFrameCalculus.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Scalar Frame Calculus.

  1. lemma OAI.KaehlerCalculus.potentialMatrix_const_add line 17
  2. lemma OAI.KaehlerCalculus.potentialMatrix_linear line 23
  3. lemma OAI.KaehlerCalculus.det_congruence_re line 31
  4. lemma OAI.KaehlerCalculus.logdet_congruence line 41
  5. lemma OAI.KaehlerCalculus.matrix_logdet_smooth line 49
  6. lemma OAI.KaehlerCalculus.potentialMatrix_logdet_pullMetric line 57
  7. lemma OAI.KaehlerCalculus.inverseTrace_pullMetric line 72