OAI/Algebra/FrobeniusObstruction/MovingCharts.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundaryOnly.FormalObstruction.movingGraphCoordinates line 16
  2. theorem OAI.BoundaryOnly.FormalObstruction.movingGraphCoordinates_pow line 22
  3. def OAI.BoundaryOnly.FormalObstruction.movingGraphSlot line 32
  4. theorem OAI.BoundaryOnly.FormalObstruction.movingGraphSlot_coordinate line 38
  5. theorem OAI.BoundaryOnly.FormalObstruction.reduce_movingGraphSlot line 43
  6. def OAI.BoundaryOnly.FormalObstruction.movingChartCoordinate line 53
  7. theorem OAI.BoundaryOnly.FormalObstruction.movingChartCoordinate_pow line 60
  8. def OAI.BoundaryOnly.FormalObstruction.movingChart line 84
  9. theorem OAI.BoundaryOnly.FormalObstruction.movingChart_coordinate line 91
  10. theorem OAI.BoundaryOnly.FormalObstruction.movingChart_specialFiber line 97
  11. theorem OAI.BoundaryOnly.FormalObstruction.movingChart_bijective line 113
  12. def OAI.BoundaryOnly.FormalObstruction.movingChartEquiv line 120
  13. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.centered_mk_pow line 134
  14. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.substitute_kernel line 143
  15. def OAI.BoundaryOnly.FormalObstruction.Frobenius.substitute line 157
  16. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.substitute_mk line 166
  17. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.substitute_coordinate line 175
  18. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.substitute_eq_eval line 183
  19. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.eval_substitute line 194
  20. def OAI.BoundaryOnly.FormalObstruction.Frobenius.planeRestriction line 217
  21. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.planeRestriction_coordinate line 225
  22. def OAI.BoundaryOnly.FormalObstruction.Frobenius.coordinatePlaneIdeal line 230
  23. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.coordinatePlaneIdeal_le_ker line 233
  24. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.planeRestriction_mod_ideal line 241
  25. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.planeRestriction_eq_zero_iff line 255
  26. def OAI.BoundaryOnly.FormalObstruction.Frobenius.chartNormalIdeal line 266
  27. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.chartNormalIdeal_mem_iff line 272
  28. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.chart_restriction_eq_zero_iff line 304