OAI/Algebra/AlgebraicObstruction/AlgebraicData.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BoundaryOnly.FormalObstruction.CoefficientRing.potential_germ line 15
  2. lemma OAI.BoundaryOnly.FormalObstruction.CoefficientRing.graphCoordinates_germ line 30
  3. lemma OAI.BoundaryOnly.FormalObstruction.CoefficientRing.graphCoordinates_constant line 37
  4. lemma OAI.BoundaryOnly.FormalObstruction.CoefficientRing.restrictedGradient_germ line 43
  5. lemma OAI.BoundaryOnly.FormalObstruction.CoefficientRing.negativeSlopeValue_germ line 50
  6. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.QuadraticData.etale_witnesses line 62
  7. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.no_algebraic_quadratic_data line 104