OAI/Geometry/NodalSets/Elliptic/IntrinsicAmbientExtension.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Yau.Target.IntrinsicTensor line 12
  2. def OAI.Yau.Target.intrinsicAmbientForm line 14
  3. def OAI.Yau.Target.intrinsicAmbientMatrix line 19
  4. lemma OAI.Yau.Target.intrinsicAmbientForm_apply line 22
  5. lemma OAI.Yau.Target.intrinsicAmbientMatrix_pairing line 27
  6. lemma OAI.Yau.Target.intrinsicAmbientMatrix_tangent line 33
  7. lemma OAI.Yau.Target.intrinsicAmbientMatrix_posDef line 39
  8. lemma OAI.Yau.Target.intrinsicAmbientMatrix_radial line 57