OAI/Algebra/AlgebraicObstruction/CoefficientData.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BoundaryOnly.FormalObstruction.CoefficientRing.SlopeVar line 11
  2. abbrev OAI.BoundaryOnly.FormalObstruction.CoefficientRing.TangentVar line 12
  3. abbrev OAI.BoundaryOnly.FormalObstruction.CoefficientRing.WallVar line 13
  4. abbrev OAI.BoundaryOnly.FormalObstruction.CoefficientRing.InternalVar line 14
  5. abbrev OAI.BoundaryOnly.FormalObstruction.CoefficientRing.GraphVar line 15
  6. abbrev OAI.BoundaryOnly.FormalObstruction.CoefficientRing.AmbientVar line 16
  7. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.originIdeal line 18
  8. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.plusCoordinates line 23
  9. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.minusCoordinates line 27
  10. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.zeroSlopes line 31
  11. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.potential line 35
  12. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.slopeDerivative line 40
  13. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.graphCoordinates line 44
  14. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.restrictedGradient line 49
  15. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.gradientIdeal line 55
  16. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.negativeSlopeValue line 60
  17. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.slope line 65
  18. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.swapBlocks line 68
  19. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.tangentMatrix line 70
  20. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.complementaryMatrix line 74
  21. structure OAI.BoundaryOnly.FormalObstruction.CoefficientRing.FormalData line 79
  22. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.map_partial line 98
  23. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.map_origin line 104
  24. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.map_mem_origin line 113
  25. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.map_mem_origin_pow line 117
  26. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.origin_constant line 123
  27. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.hasSubst_origin line 132
  28. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.plus_hasSubst line 142
  29. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.minus_hasSubst line 146
  30. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.zeroSlopes_hasSubst line 150
  31. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.map_plus line 154
  32. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.map_minus line 159
  33. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.map_zeroSlopes line 164
  34. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.map_potential line 169
  35. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.map_slopeDerivative line 175
  36. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.graph_hasSubst line 181
  37. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.map_graph line 188
  38. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.map_restrictedGradient line 194
  39. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.map_gradientIdeal line 204
  40. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.map_negativeSlopeValue line 217
  41. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.map_complementary line 228
  42. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.FormalData.map line 242
  43. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.FormalData.toField line 269