OAI/Geometry/NodalSets/Charts/MatrixMetricPullback.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Yau.Target.matrixCovariant_eq_of_entries line 11
  2. lemma OAI.Yau.Target.matrixCovariant_horizontal line 28
  3. lemma OAI.Yau.Target.matrixCovariant_round line 37
  4. lemma OAI.Yau.Target.matrixCovariant_inverse line 53
  5. lemma OAI.Yau.Target.roundCoefficients_matrix line 67
  6. lemma OAI.Yau.Target.roundCoefficients_matrix_fderiv line 73