OAI/Geometry/PrescribedPotential/MatrixFrameNormalization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Matrix Frame Normalization.

  1. def OAI.KaehlerCalculus.matrixFrame line 17
  2. lemma OAI.KaehlerCalculus.frameMatrix_matrixFrame line 20
  3. lemma OAI.KaehlerCalculus.matrixFrame_apply line 25
  4. lemma OAI.KaehlerCalculus.normalized_frame line 28
  5. lemma OAI.KaehlerCalculus.pullMetric_positive line 39
  6. lemma OAI.KaehlerCalculus.matrix_inverse_trace_congruence line 45