OAI/Algebra/AlgebraicObstruction/SeriesJets.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Close line 13
  2. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Close.refl line 16
  3. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Close.symm line 18
  4. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Close.trans line 20
  5. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Close.mono line 23
  6. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Close.zero line 26
  7. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Close.ext line 28
  8. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.iterate_step_close line 37
  9. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.iterate_later_close line 43
  10. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.fixedPoint line 52
  11. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.fixedPoint_close line 55
  12. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.fixedPoint_eq line 59
  13. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.fixedPoint_unique line 66
  14. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.exists_unique_fixedPoint line 74
  15. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Vanishes line 83
  16. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Jet line 86
  17. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Vanishes.iff_order line 88
  18. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Vanishes.zero line 94
  19. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Vanishes.mono line 96
  20. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Vanishes.add line 98
  21. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Vanishes.neg line 101
  22. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Vanishes.mul line 104
  23. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Vanishes.all line 111
  24. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Vanishes.mul_right line 113
  25. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Vanishes.mul_left line 116
  26. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Vanishes.sum line 119
  27. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Vanishes.one_iff line 125
  28. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Jet.iff_coeff line 130
  29. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Jet.refl line 133
  30. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Jet.symm line 135
  31. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Jet.trans line 137
  32. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Jet.mono line 140
  33. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Jet.neg line 142
  34. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Jet.sub line 146
  35. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.jet_iff_truncTotal line 151
  36. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Jet.subst line 164