OAI/Geometry/PrescribedRicci/DimensionOnePotential.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Dimension One Potential.

  1. lemma OAI.MongeAmpere.singleton_det_add line 18
  2. lemma OAI.MongeAmpere.singleton_posDef_of_det line 30
  3. theorem OAI.Anticanonical.SourceSmooth.dimensionOne_positiveDensity line 51
  4. theorem OAI.Anticanonical.SourceSmooth.prescribedPotential_dimensionOne line 89