OAI/Algebra/FrobeniusObstruction/FormalData.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BoundaryOnly.FormalObstruction.SlopeVar line 11
  2. abbrev OAI.BoundaryOnly.FormalObstruction.TangentVar line 12
  3. abbrev OAI.BoundaryOnly.FormalObstruction.WallVar line 13
  4. abbrev OAI.BoundaryOnly.FormalObstruction.InternalVar line 14
  5. abbrev OAI.BoundaryOnly.FormalObstruction.GraphVar line 15
  6. abbrev OAI.BoundaryOnly.FormalObstruction.AmbientVar line 16
  7. def OAI.BoundaryOnly.FormalObstruction.originIdeal line 18
  8. def OAI.BoundaryOnly.FormalObstruction.plusCoordinates line 23
  9. def OAI.BoundaryOnly.FormalObstruction.minusCoordinates line 27
  10. def OAI.BoundaryOnly.FormalObstruction.zeroSlopes line 31
  11. def OAI.BoundaryOnly.FormalObstruction.potential line 35
  12. def OAI.BoundaryOnly.FormalObstruction.slopeDerivative line 40
  13. def OAI.BoundaryOnly.FormalObstruction.graphCoordinates line 44
  14. def OAI.BoundaryOnly.FormalObstruction.restrictedGradient line 49
  15. def OAI.BoundaryOnly.FormalObstruction.gradientIdeal line 55
  16. def OAI.BoundaryOnly.FormalObstruction.negativeSlopeValue line 60
  17. def OAI.BoundaryOnly.FormalObstruction.slope line 65
  18. def OAI.BoundaryOnly.FormalObstruction.swapBlocks line 68
  19. def OAI.BoundaryOnly.FormalObstruction.tangentMatrix line 70
  20. def OAI.BoundaryOnly.FormalObstruction.complementaryMatrix line 75
  21. structure OAI.BoundaryOnly.FormalObstruction.FormalData line 81