OAI/Algebra/FrobeniusObstruction/GraphPotential.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BoundaryOnly.FormalObstruction.ParameterScalar line 14
  2. def OAI.BoundaryOnly.FormalObstruction.normalIndices line 16
  3. theorem OAI.BoundaryOnly.FormalObstruction.mem_normalIndices line 18
  4. def OAI.BoundaryOnly.FormalObstruction.normalPlane line 21
  5. theorem OAI.BoundaryOnly.FormalObstruction.normalPlane_coordinate line 26
  6. theorem OAI.BoundaryOnly.FormalObstruction.normalPlane_movingGraphSlot line 31
  7. theorem OAI.BoundaryOnly.FormalObstruction.normalPlane_smul line 44
  8. theorem OAI.BoundaryOnly.FormalObstruction.normalPlane_fixedComplement line 49
  9. def OAI.BoundaryOnly.FormalObstruction.ambientCoordinates line 55
  10. theorem OAI.BoundaryOnly.FormalObstruction.ambientCoordinates_pow line 61
  11. def OAI.BoundaryOnly.FormalObstruction.ambientSlot line 71
  12. theorem OAI.BoundaryOnly.FormalObstruction.ambientSlot_coordinate line 76
  13. theorem OAI.BoundaryOnly.FormalObstruction.graphCoordinates_constant_zero line 81
  14. def OAI.BoundaryOnly.FormalObstruction.formalGraph line 87
  15. theorem OAI.BoundaryOnly.FormalObstruction.formalGraph_mk line 92
  16. theorem OAI.BoundaryOnly.FormalObstruction.graph_restriction_hom line 98
  17. def OAI.BoundaryOnly.FormalObstruction.movingPotential line 120
  18. theorem OAI.BoundaryOnly.FormalObstruction.movingPotential_graph_zero line 124
  19. theorem OAI.BoundaryOnly.FormalObstruction.partial_ambientCoordinates line 142
  20. theorem OAI.BoundaryOnly.FormalObstruction.parameter_chain_rule line 156
  21. theorem OAI.BoundaryOnly.FormalObstruction.sum_mul_single line 168
  22. theorem OAI.BoundaryOnly.FormalObstruction.partial_ambientSlot line 173
  23. theorem OAI.BoundaryOnly.FormalObstruction.movingPotential_restricted_partial line 182
  24. theorem OAI.BoundaryOnly.FormalObstruction.normalPlane_slot_apply line 200
  25. theorem OAI.BoundaryOnly.FormalObstruction.movingPotential_mem_normalIdeal line 206
  26. theorem OAI.BoundaryOnly.FormalObstruction.graphIdeal_ambient_discrepancy line 217