OAI/Algebra/FrobeniusObstruction/NormalPrimitives.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundaryOnly.FormalObstruction.Frobenius.normalCoordinateList line 19
  2. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.normalCoordinateList_span line 25
  3. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.normalCoordinateList_pow line 35
  4. def OAI.BoundaryOnly.FormalObstruction.Frobenius.chartNormal line 42
  5. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.chartNormal_d line 47
  6. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.chartNormal_annihilate line 52
  7. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.chartNormal_delta line 59
  8. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.chartNormal_primitive line 67
  9. abbrev OAI.BoundaryOnly.FormalObstruction.ParameterForms line 87
  10. def OAI.BoundaryOnly.FormalObstruction.parameterPartial line 90
  11. theorem OAI.BoundaryOnly.FormalObstruction.parameterPartial_apply line 96
  12. theorem OAI.BoundaryOnly.FormalObstruction.parameterPartial_commute line 101
  13. def OAI.BoundaryOnly.FormalObstruction.movingNormal line 106
  14. theorem OAI.BoundaryOnly.FormalObstruction.movingNormal_d line 113
  15. theorem OAI.BoundaryOnly.FormalObstruction.movingNormal_delta line 119
  16. theorem OAI.BoundaryOnly.FormalObstruction.movingNormal_annihilate line 127
  17. theorem OAI.BoundaryOnly.FormalObstruction.movingNormal_primitive line 137
  18. theorem OAI.BoundaryOnly.FormalObstruction.movingNormal_cubic_primitive line 154
  19. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.series_pderiv_map line 187
  20. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.mapCoefficients_partial line 194
  21. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.baseChange_partial line 203
  22. def OAI.BoundaryOnly.FormalObstruction.MixedForms.coefficientMap line 217
  23. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.coefficientMap_tmul line 222
  24. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.coefficientMap_coeff line 227
  25. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.coefficientMap_d line 230
  26. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.coefficientMap_gradient line 239
  27. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.coefficientMap_delta line 245
  28. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.coefficientMap_cartier line 252
  29. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.coefficientMap_normal line 259
  30. theorem OAI.BoundaryOnly.FormalObstruction.movingChart_inverse_specialFiber line 277
  31. def OAI.BoundaryOnly.FormalObstruction.specialNormal line 291
  32. theorem OAI.BoundaryOnly.FormalObstruction.reduce_normalList line 296
  33. theorem OAI.BoundaryOnly.FormalObstruction.reduce_movingNormal line 306
  34. def OAI.BoundaryOnly.FormalObstruction.specialAmbient line 327
  35. theorem OAI.BoundaryOnly.FormalObstruction.specialAmbient_slope line 336
  36. theorem OAI.BoundaryOnly.FormalObstruction.specialAmbient_internal line 341
  37. theorem OAI.BoundaryOnly.FormalObstruction.reduce_ambientSlot line 345
  38. def OAI.BoundaryOnly.FormalObstruction.specialPotential line 359
  39. theorem OAI.BoundaryOnly.FormalObstruction.reduce_movingPotential line 363
  40. theorem OAI.BoundaryOnly.FormalObstruction.specialNormal_d line 369
  41. theorem OAI.BoundaryOnly.FormalObstruction.parameter_reduction_partial line 374
  42. theorem OAI.BoundaryOnly.FormalObstruction.specialNormal_delta line 379
  43. theorem OAI.BoundaryOnly.FormalObstruction.specialNormal_primitive line 389